Basic facts about matrices (over a commutative ring) and the determinant.
The (n by n) matrices form a ring (see matrix-ring_wf).
The determinant satisfies |AB| = |A|*|B| (see det-times).
The determinant is defined using the "Liebnitz" form matrix-det,
but we prove the "Laplace" formula for expanding a determinant by minors
(see matrix-det-is-determinant)
Matrix A is invertible iff |A| is invertible in the ring
(invertible-matrix-iff-det)
and inverses are unique
(invertible-matrix-iff-left, inverse-unique).
When |A| is invertible in the ring then we have Cramer's rule
(Cramers-rule).⋅
Definition: rng_lsum
Σ{r} x ∈ as. f[x] == reduce(+r;0;map(λx.f[x];as))
Lemma: rng_lsum_wf
∀[r:Rng]. ∀[A:Type]. ∀[f:A ⟶ |r|]. ∀[as:A List]. (Σ{r} x ∈ as. f[x] ∈ |r|)
Lemma: rng_lsum_nil_lemma
∀f,r:Top. (Σ{r} x ∈ []. f[x] ~ 0)
Lemma: rng_lsum_cons_lemma
∀f,v,u,r:Top. (Σ{r} x ∈ [u / v]. f[x] ~ f[u] +r Σ{r} x ∈ v. f[x])
Lemma: rng_lsum_functionality_wrt_permutation
∀[r:Rng]. ∀[A:Type]. ∀[f:A ⟶ |r|]. ∀[as,bs:A List].
Σ{r} x ∈ as. f[x] = Σ{r} x ∈ bs. f[x] ∈ |r| supposing permutation(A;as;bs)
Lemma: rng_minus_lsum
∀r:Rng. ∀A:Type. ∀as:A List. ∀f:A ⟶ |r|. ((-r Σ{r} x ∈ as. f[x]) = Σ{r} x ∈ as. (-r f[x]) ∈ |r|)
Lemma: rng_lsum_0
∀r:Rng. ∀A:Type. ∀as:A List. (Σ{r} x ∈ as. 0 = 0 ∈ |r|)
Lemma: rng_lsum_plus
∀[r:Rng]. ∀[A:Type]. ∀[f,g:A ⟶ |r|]. ∀[as:A List].
(Σ{r} x ∈ as. (f[x] +r g[x]) = (Σ{r} x ∈ as. f[x] +r Σ{r} x ∈ as. g[x]) ∈ |r|)
Lemma: rng_times_lsum_l
∀r:Rng. ∀A:Type. ∀as:A List. ∀f:A ⟶ |r|. ∀u:|r|. ((u * Σ{r} x ∈ as. f[x]) = Σ{r} x ∈ as. (u * f[x]) ∈ |r|)
Lemma: rng_times_lsum_r
∀r:Rng. ∀A:Type. ∀as:A List. ∀f:A ⟶ |r|. ∀u:|r|. ((Σ{r} x ∈ as. f[x] * u) = Σ{r} x ∈ as. (f[x] * u) ∈ |r|)
Lemma: rng_lsum_when_swap
∀r:Rng. ∀A:Type. ∀f:A ⟶ |r|. ∀b:𝔹. ∀as:A List. (Σ{r} x ∈ as. (when b. f[x]) = (when b. Σ{r} x ∈ as. f[x]) ∈ |r|)
Lemma: rng_lsum_swap
∀[r:Rng]. ∀[A,B:Type]. ∀[F:A ⟶ B ⟶ |r|]. ∀[as:A List]. ∀[bs:B List].
(Σ{r} a ∈ as. Σ{r} b ∈ bs. F[a;b] = Σ{r} b ∈ bs. Σ{r} a ∈ as. F[a;b] ∈ |r|)
Lemma: rng_lsum_map
∀[r:Rng]. ∀[A,B:Type]. ∀[g:A ⟶ B]. ∀f:B ⟶ |r|. ∀as:A List. (Σ{r} x ∈ map(g;as). f[x] = Σ{r} x ∈ as. f[g x] ∈ |r|)
Lemma: rng_lsum-split
∀[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[r:Rng]. ∀[f:A ⟶ |r|]. ∀[as:A List].
(Σ{r} x ∈ as. f[x] = (Σ{r} x ∈ filter(p;as). f[x] +r Σ{r} x ∈ filter(λa.(¬b(p a));as). f[x]) ∈ |r|)
Lemma: rng_lsum-partition
∀[k:ℕ]. ∀[A:Type]. ∀[p:A ⟶ ℕk]. ∀[r:Rng]. ∀[f:A ⟶ |r|]. ∀[as:A List].
(Σ{r} x ∈ as. f[x] = (Σ(r) 0 ≤ i < k. Σ{r} x ∈ filter(λa.(p a =z i);as). f[x]) ∈ |r|)
Lemma: rng_lsum-from-upto
∀[a,b:ℤ]. ∀[r:Rng]. ∀[f:{a..b-} ⟶ |r|]. (Σ{r} x ∈ [a, b). f[x] = (Σ(r) a ≤ i < b. f[i]) ∈ |r|)
Lemma: rng_lsum-upto
∀[n:ℤ]. ∀[r:Rng]. ∀[f:ℕn ⟶ |r|]. (Σ{r} x ∈ upto(n). f[x] = (Σ(r) 0 ≤ i < n. f[i]) ∈ |r|)
Lemma: rng_prod_injection
∀[r:CRng]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. ∀[f:ℕn →⟶ ℕn]. ((Π(r) 0 ≤ i < n. F[i]) = (Π(r) 0 ≤ i < n. F[f i]) ∈ |r|)
Lemma: rng_prod_unroll_base
∀[r,F:Top]. (Π(r) 0 ≤ i < 0. F[i] ~ 1)
Lemma: rng_prod_unroll_hi
∀[r:CRng]. ∀[n:ℕ+]. ∀[F:ℕn ⟶ |r|]. ((Π(r) 0 ≤ i < n. F[i]) = ((Π(r) 0 ≤ i < n - 1. F[i]) * F[n - 1]) ∈ |r|)
Lemma: rng_prod_1
∀[r:CRng]. ∀[n:ℕ]. ((Π(r) 0 ≤ i < n. 1) = 1 ∈ |r|)
Lemma: rng_prod_empty_lemma
∀f,r:Top. (Π(r) 0 ≤ i < 0. f[i] ~ 1)
Lemma: rng_prod_plus
∀[r:CRng]. ∀[n:ℕ]. ∀[F,G:ℕn ⟶ |r|].
((Π(r) 0
≤ i
< n
F[i] +r G[i])
= Σ{r} p ∈ functions-list(n;2). (Π(r) 0
≤ i
< n
if (p i =z 0) then F[i] else G[i] fi )
∈ |r|)
Lemma: rng_prod_const_mul
∀[r:CRng]. ∀[c:|r|]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. ((Π(r) 0 ≤ i < n. F[i] * c) = ((c ↑r n) * (Π(r) 0 ≤ i < n. F[i])) ∈ |r|)
Definition: matrix
Matrix(n;m;r) == ℕn ⟶ ℕm ⟶ |r|
Lemma: matrix_wf
∀[n,m:ℤ]. ∀[r:RngSig]. (Matrix(n;m;r) ∈ Type)
Definition: matrix-ap
M[i,j] == M i j
Lemma: matrix-ap_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i:ℕn]. ∀[j:ℕm]. ∀[M:Matrix(n;m;r)]. (M[i,j] ∈ |r|)
Definition: mx
matrix(M[x; y]) == λx,y. M[x; y]
Lemma: mx_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[M:ℕn ⟶ ℕm ⟶ |r|]. (matrix(M[x;y]) ∈ Matrix(n;m;r))
Lemma: matrix_ap_mx_lemma
∀j,i,M:Top. (matrix(M[x;y])[i,j] ~ M[i;j])
Definition: matrix-transpose
M' == matrix(M[y,x])
Lemma: matrix-transpose_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[M:Matrix(n;m;r)]. (M' ∈ Matrix(m;n;r))
Lemma: matrix-transpose-twice
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[M:Matrix(n;m;r)]. (M'' = M ∈ Matrix(n;m;r))
Definition: matrix-swap-rows
matrix-swap-rows(M;i;j) == matrix(M[if x=i then j else if x=j then i else x,y])
Lemma: matrix-swap-rows_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i,j:ℕn]. ∀[M:Matrix(n;m;r)]. (matrix-swap-rows(M;i;j) ∈ Matrix(n;m;r))
Definition: matrix-swap-cols
matrix-swap-cols(M;i;j) == matrix(M[x,if y=i then j else if y=j then i else y])
Lemma: matrix-swap-cols_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i,j:ℕm]. ∀[M:Matrix(n;m;r)]. (matrix-swap-cols(M;i;j) ∈ Matrix(n;m;r))
Definition: matrix-mul-col
matrix-mul-col(r;k;i;M) == matrix(if y=i then k * M[x,y] else M[x,y])
Lemma: matrix-mul-col_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[k:|r|]. ∀[i:ℕm]. ∀[M:Matrix(n;m;r)]. (matrix-mul-col(r;k;i;M) ∈ Matrix(n;m;r))
Definition: matrix-mul-row
matrix-mul-row(r;k;i;M) == matrix(if x=i then k * M[x,y] else M[x,y])
Lemma: matrix-mul-row_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[k:|r|]. ∀[i:ℕn]. ∀[M:Matrix(n;m;r)]. (matrix-mul-row(r;k;i;M) ∈ Matrix(n;m;r))
Definition: matrix-plus
M + N == matrix(M[x,y] +r N[x,y])
Lemma: matrix-plus_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[M,N:Matrix(n;m;r)]. (M + N ∈ Matrix(n;m;r))
Lemma: matrix-plus-assoc
∀[n,m:ℤ]. ∀[r:Rng]. ∀[M,N,K:Matrix(n;m;r)]. (M + N + K = M + N + K ∈ Matrix(n;m;r))
Lemma: matrix-plus-comm
∀[n,m:ℤ]. ∀[r:Rng]. ∀[M,N:Matrix(n;m;r)]. (M + N = N + M ∈ Matrix(n;m;r))
Definition: matrix-times
(M*N) == matrix(Σ(r) 0 ≤ i < n. M[x,i] * N[i,y])
Lemma: matrix-times_wf
∀[n,k,m:ℤ]. ∀[r:Rng]. ∀[M:Matrix(n;k;r)]. ∀[N:Matrix(k;m;r)]. ((M*N) ∈ Matrix(n;m;r))
Lemma: matrix-times-assoc
∀[n,k,m,l:ℕ]. ∀[r:Rng]. ∀[M:Matrix(n;k;r)]. ∀[N:Matrix(k;m;r)]. ∀[K:Matrix(m;l;r)].
(((M*N)*K) = (M*(N*K)) ∈ Matrix(n;l;r))
Lemma: matrix-times-distrib-left
∀[n,k,m:ℕ]. ∀[r:Rng]. ∀[M:Matrix(n;k;r)]. ∀[N,K:Matrix(k;m;r)]. ((M*N + K) = (M*N) + (M*K) ∈ Matrix(n;m;r))
Lemma: matrix-times-distrib-right
∀[n,k,m:ℕ]. ∀[r:Rng]. ∀[M,N:Matrix(n;k;r)]. ∀[K:Matrix(k;m;r)]. ((M + N*K) = (M*K) + (N*K) ∈ Matrix(n;m;r))
Lemma: matrix-transpose-times
∀[n,k,m:ℕ]. ∀[r:CRng]. ∀[M:Matrix(n;k;r)]. ∀[N:Matrix(k;m;r)]. ((M*N)' = (N'*M') ∈ Matrix(m;n;r))
Definition: identity-matrix
I == matrix(if x=y then 1 else 0)
Lemma: identity-matrix_wf
∀[n,m:ℤ]. ∀[r:RngSig]. (I ∈ Matrix(n;m;r))
Definition: zero-matrix
0 == matrix(0)
Lemma: zero-matrix_wf
∀[m,n:ℤ]. ∀[r:RngSig]. (0 ∈ Matrix(n;m;r))
Definition: J-matrix
J == matrix(1)
Lemma: J-matrix_wf
∀[m,n:ℤ]. ∀[r:RngSig]. (J ∈ Matrix(n;m;r))
Definition: matrix-minus
-(M) == matrix(-r M[x,y])
Lemma: matrix-minus_wf
∀[m,n:ℤ]. ∀[r:RngSig]. ∀[M:Matrix(n;m;r)]. (-(M) ∈ Matrix(n;m;r))
Lemma: matrix-times-id-left
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. ((I*N) = N ∈ Matrix(k;m;r))
Lemma: matrix-times-0-right
∀[k,m,n:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. ((N*0) = 0 ∈ Matrix(k;n;r))
Lemma: matrix-plus-zero-left
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. (0 + N = N ∈ Matrix(k;m;r))
Lemma: matrix-plus-minus-left
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. (-(N) + N = 0 ∈ Matrix(k;m;r))
Lemma: matrix-times-id-right
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. ((N*I) = N ∈ Matrix(k;m;r))
Lemma: matrix-times-0-left
∀[k,m,n:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. ((0*N) = 0 ∈ Matrix(n;m;r))
Lemma: matrix-plus-zero-right
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. (N + 0 = N ∈ Matrix(k;m;r))
Lemma: matrix-plus-minus-right
∀[k,m:ℕ]. ∀[r:Rng]. ∀[N:Matrix(k;m;r)]. (N + -(N) = 0 ∈ Matrix(k;m;r))
Definition: matrix-ring
matrix-ring(r;n) == <Matrix(n;n;r), λu,v. ff, λu,v. ff, λM,N. M + N, 0, λM.-(M), λM,N. (M*N), I, λu,v. (inr ⋅ )>
Lemma: matrix-ring_wf
∀[r:Rng]. ∀[n:ℕ]. (matrix-ring(r;n) ∈ Rng)
Definition: matrix-det
|M| == Σ{r} f ∈ permutations-list(n). let k = Π(r) 0 ≤ i < n. M[i,f i] in if permutation-sign(n;f)=1 then k else (-r k)
Lemma: matrix-det_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. (|M| ∈ |r|)
Lemma: matrix-det-dim0
∀[r:Rng]. ∀[M:Top]. (|M| = 1 ∈ |r|)
Lemma: matrix-det-dim1
∀[r:CRng]. ∀[M:Row(1;r)]. (|M| = M[0,0] ∈ |r|)
Lemma: det-transpose
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. (|M'| = |M| ∈ |r|)
Lemma: det-id
∀[r:CRng]. ∀[n:ℕ]. (|I| = 1 ∈ |r|)
Lemma: det-swap-cols
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn]. |matrix-swap-cols(M;i;j)| = (-r |M|) ∈ |r| supposing ¬(i = j ∈ ℤ)
Lemma: det-equal-rows
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn].
|M| = 0 ∈ |r| supposing (¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r))
Lemma: equal-rows-det
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].
|M| = 0 ∈ |r| supposing ∃i,j:ℕn. ((¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)))
Lemma: swap-rows-is-transpose-swap-cols
∀[M,i,j:Top]. (matrix-swap-rows(M;i;j) ~ matrix-swap-cols(M';i;j)')
Lemma: mul-row-is-transpose-mul-col
∀[M,r,i,k:Top]. (matrix-mul-row(r;k;i;M) ~ matrix-mul-col(r;k;i;M')')
Lemma: mul-col-is-transpose-mul-row
∀[M,r,i,k:Top]. (matrix-mul-col(r;k;i;M) ~ matrix-mul-row(r;k;i;M')')
Lemma: det-mul-row
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[k:|r|]. (|matrix-mul-row(r;k;i;M)| = (k * |M|) ∈ |r|)
Lemma: det-mul-col
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[k:|r|]. (|matrix-mul-col(r;k;i;M)| = (k * |M|) ∈ |r|)
Lemma: det-swap-rows
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn]. |matrix-swap-rows(M;i;j)| = (-r |M|) ∈ |r| supposing ¬(i = j ∈ ℤ)
Lemma: det-add-row
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[row:ℕn ⟶ |r|].
(|matrix(if x=i then (row y) +r M[x,y] else M[x,y])| = (|matrix(if x=i then row y else M[x,y])| +r |M|) ∈ |r|)
Definition: det-fun
These properties characterize the determinant up to a multiplicative constant.
⌜λM.|M|⌝ is such a function (see matrix-det-is-det-fun)
and we prove that any such function d is equal to
λM.((d I) * (determinant(n;r) M))
where the primitive recursive function ⌜determinant(n;r)⌝
expands by minors of the first row.
(see det-fun-is-determinant)
A corollary is that the two versions of the determinant
(the "Leibnitz" form
|M| == Σ{r} f ∈ permutations-list(n). let k = Π(r) 0 ≤ i < n. M[i,f i] in if permutation-sign(n;f)=1 then k else (-r k)
and the "Laplace" form
determinant(n;r) ==
primrec(n;λm.1;λn',d,m. (Σ(r) 0 ≤ i < n' + 1. if isEven(i) then m[0,i] else -r m[0,i] fi * (d matrix-minor(0;i;m))))
are equal (matrix-det-is-determinant).
We include the property that when two distinct rows are equal then
the determinant is 0, because for rings of characteristic 2, this does
not follow from the property that swapping rows reverses the sign.
.⋅
det-fun(r;n) ==
{d:Matrix(n;n;r) ⟶ |r||
(∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|))
∧ (∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|))
∧ (∀i,j:ℕn. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|))))
∧ (∀i,j:ℕn.
((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)) ⇒ ((d M) = 0 ∈ |r|)))))}
Lemma: det-fun_wf
∀[r:Rng]. ∀[n:ℕ]. (det-fun(r;n) ∈ Type)
Lemma: det-fun-zero-row
∀[r:Rng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)]. ∀[M:Matrix(n;n;r)]. (d M) = 0 ∈ |r| supposing ∃i:ℕn. ∀j:ℕn. (M[i,j] = 0 ∈ |r|)
Definition: row-op
row-op(r;a;b;k;M) == matrix(if x=a then M[x,y] +r (k * M[b,y]) else M[x,y])
Lemma: row-op_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[k:|r|]. ∀[a,b:ℕn]. ∀[M:Matrix(n;m;r)]. (row-op(r;a;b;k;M) ∈ Matrix(n;m;r))
Lemma: det-fun-row-op
∀[r:Rng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)]. ∀[M:Matrix(n;n;r)]. ∀[a,b:ℕn]. ∀[k:|r|].
(d row-op(r;a;b;k;M)) = (d M) ∈ |r| supposing ¬(a = b ∈ ℤ)
Lemma: matrix-det-is-det-fun
∀[r:CRng]. ∀[n:ℕ]. (λM.|M| ∈ det-fun(r;n))
Lemma: det-row-op
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a,b:ℕn]. ∀[k:|r|]. |row-op(r;a;b;k;M)| = |M| ∈ |r| supposing ¬(a = b ∈ ℤ)
Lemma: det-multiple-row-ops
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a:ℕn]. ∀[k:|r|].
(|matrix(if x=a then M[x,y] else (M[x,y] +r (k * M[a,y])))| = |M| ∈ |r|)
Lemma: det-multiple-col-ops
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a:ℕn]. ∀[k:|r|].
(|matrix(if y=a then M[x,y] else (M[x,y] +r (k * M[x,a])))| = |M| ∈ |r|)
Definition: matrix-minor
The minor of an (n by m) matrix is an (n-1 by m-1) matrix obtained
by deleting row i and column j.⋅
matrix-minor(i;j;m) == λx,y. m[if (x) < (i) then x else (x + 1),if (y) < (j) then y else (y + 1)]
Lemma: matrix-minor_wf
∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i:ℕn]. ∀[j:ℕm]. ∀[M:Matrix(n;m;r)]. (matrix-minor(i;j;M) ∈ Matrix(n - 1;m - 1;r))
Lemma: transpose-matrix-minor
∀[i,j,M:Top]. (matrix-minor(i;j;M)' ~ matrix-minor(j;i;M'))
Definition: matrix+
matrix+(r;j;M) ==
matrix(if x=0
then if y=j then 1 else 0
else if (y) < (j) then M[x - 1,y] else if (j) < (y) then M[x - 1,y - 1] else 0)
Lemma: matrix+_wf
∀[n,m:ℤ]. ∀[j:ℕm + 1]. ∀[r:RngSig]. ∀[M:Matrix(n;m;r)]. (matrix+(r;j;M) ∈ Matrix(n + 1;m + 1;r))
Lemma: det-fun+
∀[n:ℕ]. ∀[J:ℕn + 1]. ∀[r:Rng]. ∀[d:det-fun(r;n + 1)]. (λM.(d matrix+(r;J;M)) ∈ det-fun(r;n))
Lemma: det-fun+-at-identity
∀[n:ℕ]. ∀[J:ℕn + 1]. ∀[r:Rng]. ∀[d:det-fun(r;n + 1)].
((d matrix+(r;J;I)) = if isEven(J) then d I else -r (d I) fi ∈ |r|)
Definition: determinant
determinant(n;r) ==
primrec(n;λm.1;λn',d,m. (Σ(r) 0 ≤ i < n' + 1. if isEven(i) then m[0,i] else -r m[0,i] fi * (d matrix-minor(0;i;m))))
Lemma: determinant_wf
∀[r:CRng]. ∀[n:ℕ]. (determinant(n;r) ∈ Matrix(n;n;r) ⟶ |r|)
Lemma: det-fun-is-determinant
∀[r:CRng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)]. (d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|))
Lemma: matrix-det-is-determinant
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. (|M| = (determinant(n;r) M) ∈ |r|)
Definition: diagonal-matrix
diagonal-matrix(r;x.F[x]) == matrix(if x=y then F[x] else 0)
Lemma: diagonal-matrix_wf
∀[r:RngSig]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. (diagonal-matrix(r;i.F[i]) ∈ Matrix(n;n;r))
Lemma: det-times
∀[r:CRng]. ∀[n:ℕ]. ∀[A,B:Matrix(n;n;r)]. (|(A*B)| = (|A| * |B|) ∈ |r|)
Definition: matrix-scalar-mul
k*M == matrix(k * M[x,y])
Lemma: matrix-scalar-mul_wf
∀[r:RngSig]. ∀[k:|r|]. ∀[n,m:ℕ]. ∀[M:Matrix(n;m;r)]. (k*M ∈ Matrix(n;m;r))
Lemma: matrix-scalar-mul-mul
∀[n,m:ℕ]. ∀[r:Rng]. ∀[k1,k2:|r|]. ∀[M:Matrix(n;m;r)]. (k1*k2*M = k1 * k2*M ∈ Matrix(n;m;r))
Lemma: matrix-scalar-mul-1
∀[n,m:ℕ]. ∀[r:Rng]. ∀[M:Matrix(n;m;r)]. (1*M = M ∈ Matrix(n;m;r))
Lemma: matrix-times-scalar-mul
∀[n,k,m:ℕ]. ∀[r:CRng]. ∀[A:Matrix(n;k;r)]. ∀[B:Matrix(k;m;r)]. ∀[c:|r|]. ((A*c*B) = c*(A*B) ∈ Matrix(n;m;r))
Lemma: matrix-scalar-mul-times
∀[n,k,m:ℕ]. ∀[r:Rng]. ∀[A:Matrix(n;k;r)]. ∀[B:Matrix(k;m;r)]. ∀[c:|r|]. ((c*A*B) = c*(A*B) ∈ Matrix(n;m;r))
Lemma: transpose-scalar-mul
∀[r,k,M:Top]. (k*M' ~ k*M')
Lemma: transpose-identity-matrix
∀[r:RngSig]. ∀[n:ℕ]. (I' = I ∈ Matrix(n;n;r))
Definition: adjugate
adj(M) == matrix(if isEven(x + y) then |matrix-minor(y;x;M)| else -r |matrix-minor(y;x;M)| fi )
Lemma: adjugate_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. (adj(M) ∈ Matrix(n;n;r))
Lemma: adjugate-property
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ((M*adj(M)) = |M|*I ∈ Matrix(n;n;r))
Lemma: adjugate-transpose
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. (adj(M') = adj(M)' ∈ Matrix(n;n;r))
Lemma: adjugate-property2
∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ((adj(M)*M) = |M|*I ∈ Matrix(n;n;r))
Lemma: null-space-unique
∀[r:IntegDom{i}]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].
∀[u:Column(n;r)]. (((M*u) = 0 ∈ Column(n;r)) ⇒ (u = 0 ∈ Column(n;r))) supposing ¬(|M| = 0 ∈ |r|)
Lemma: expand-det-by-column
∀[n:ℕ]. ∀[j:ℕn]. ∀[r:CRng]. ∀[M:Matrix(n;n;r)].
(|M| = (Σ(r) 0 ≤ i < n. if isEven(i + j) then M[i,j] else -r M[i,j] fi * |matrix-minor(i;j;M)|) ∈ |r|)
Lemma: expand-det-by-row
∀[n:ℕ]. ∀[i:ℕn]. ∀[r:CRng]. ∀[M:Matrix(n;n;r)].
(|M| = (Σ(r) 0 ≤ j < n. if isEven(i + j) then M[i,j] else -r M[i,j] fi * |matrix-minor(i;j;M)|) ∈ |r|)
Lemma: det-diagonal
∀[r:CRng]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. (|diagonal-matrix(r;i.F[i])| = (Π(r) 0 ≤ i < n. F[i]) ∈ |r|)
Lemma: det-kI+J
∀[r:CRng]. ∀[n:ℕ]. ∀[a:|r|]. (|a*I + J| = if (n =z 0) then 1 else (a +r int-to-ring(r;n)) * (a ↑r (n - 1)) fi ∈ |r|)
Definition: invertible-matrix
invertible-matrix(r;n;A) == ∃B:Matrix(n;n;r). ((A*B) = I ∈ Matrix(n;n;r))
Lemma: invertible-matrix_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. (invertible-matrix(r;n;A) ∈ ℙ)
Lemma: invertible-matrix-iff-det
∀r:CRng. ∀n:ℕ. ∀A:Matrix(n;n;r). (invertible-matrix(r;n;A) ⇐⇒ |A| | 1 in r)
Lemma: invertible-matrix-iff-left
∀r:CRng. ∀n:ℕ. ∀A:Matrix(n;n;r). (invertible-matrix(r;n;A) ⇐⇒ ∃B:Matrix(n;n;r). ((B*A) = I ∈ Matrix(n;n;r)))
Lemma: inverse-unique
∀[r:CRng]. ∀[n:ℕ]. ∀[A,B,C:Matrix(n;n;r)].
((((A*B) = I ∈ Matrix(n;n;r)) ∨ ((B*A) = I ∈ Matrix(n;n;r)))
⇒ (((A*C) = I ∈ Matrix(n;n;r)) ∨ ((C*A) = I ∈ Matrix(n;n;r)))
⇒ (B = C ∈ Matrix(n;n;r)))
Definition: adj-solution
adj-solution(r;n;A;c;b) == c*(adj(A)*b)
Lemma: adj-solution_wf
∀[r:CRng]. ∀[n,m:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:|r|]. ∀[b:Matrix(n;m;r)]. (adj-solution(r;n;A;c;b) ∈ Matrix(n;m;r))
Lemma: adj-solution-property
∀[r:CRng]. ∀[n,m:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:|r|]. ∀[b:Matrix(n;m;r)].
(A*adj-solution(r;n;A;c;b)) = b ∈ Matrix(n;m;r) supposing (c * |A|) = 1 ∈ |r|
Lemma: adj-solution-column
∀[r:CRng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:|r|]. ∀[b:Column(n;r)].
(adj-solution(r;n;A;c;b) = c*matrix(|matrix(if y=j then b[x,0] else A[x,y])|) ∈ Column(n;r))
Lemma: Cramers-rule
∀[r:CRng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:{c:|r|| (c * |A|) = 1 ∈ |r|} ]. ∀[b:Column(n;r)].
((A*c*matrix(|matrix(if y=j then b[x,0] else A[x,y])|)) = b ∈ Column(n;r))
Definition: vector-add
(a + b) == λi.((a i) +r (b i))
Lemma: vector-add_wf
∀[i:Type]. ∀[r:RngSig]. ∀[a,b:i ⟶ |r|]. ((a + b) ∈ i ⟶ |r|)
Definition: vector-mul
(c*a) == λi.(c * (a i))
Lemma: vector-mul_wf
∀[i:Type]. ∀[r:RngSig]. ∀[c:|r|]. ∀[a:i ⟶ |r|]. ((c*a) ∈ i ⟶ |r|)
Lemma: vector-mul-mul
∀[i:Type]. ∀[r:Rng]. ∀[c1,c2:|r|]. ∀[a:i ⟶ |r|]. ((c1*(c2*a)) = (c1 * c2*a) ∈ (i ⟶ |r|))
Definition: zero-vector
0 == λi.0
Lemma: zero-vector_wf
∀[i:Type]. ∀[r:RngSig]. (0 ∈ i ⟶ |r|)
Lemma: mul-zero-vector
∀[i:Type]. ∀[r:Rng]. ∀[c:|r|]. ((c*0) = 0 ∈ (i ⟶ |r|))
Lemma: zero-vector-add-left
∀[i:Type]. ∀[r:Rng]. ∀[a:i ⟶ |r|]. ((0 + a) = a ∈ (i ⟶ |r|))
Lemma: zero-vector-add-right
∀[i:Type]. ∀[r:Rng]. ∀[a:i ⟶ |r|]. ((a + 0) = a ∈ (i ⟶ |r|))
Definition: cross-product
(a x b) ==
λi.[((a 1) * (b 2)) +r (-r ((a 2) * (b 1)));
((a 2) * (b 0)) +r (-r ((a 0) * (b 2)));
((a 0) * (b 1)) +r (-r ((a 1) * (b 0)))][i]
Lemma: cross-product_wf
∀[r:RngSig]. ∀[a,b:ℕ3 ⟶ |r|]. ((a x b) ∈ ℕ3 ⟶ |r|)
Lemma: cross-product-same
∀[r:CRng]. ∀[a:ℕ3 ⟶ |r|]. ((a x a) = 0 ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-anti-comm
∀[r:CRng]. ∀[a,b:ℕ3 ⟶ |r|]. ((b x a) = (-r 1*(a x b)) ∈ (ℕ3 ⟶ |r|))
Lemma: Jacobi-identity
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (((a x (b x c)) + ((b x (c x a)) + (c x (a x b)))) = 0 ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-distrib1
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. ((a x (b + c)) = ((a x b) + (a x c)) ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-distrib2
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (((b + c) x a) = ((b x a) + (c x a)) ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-mul1
∀[r:CRng]. ∀[a,b:ℕ3 ⟶ |r|]. ∀[c:|r|]. (((c*a) x b) = (c*(a x b)) ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-mul2
∀[r:CRng]. ∀[a,b:ℕ3 ⟶ |r|]. ∀[c:|r|]. ((a x (c*b)) = (c*(a x b)) ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-0
∀[r:Rng]. ∀[a:ℕ3 ⟶ |r|]. ((a x 0) = 0 ∈ (ℕ3 ⟶ |r|))
Lemma: cross-product-equal-zero
∀r:IntegDom{i}. ∀a,b:ℕ3 ⟶ |r|.
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ ((a x b) = 0 ∈ (ℕ3 ⟶ |r|)
⇐⇒ (a = 0 ∈ (ℕ3 ⟶ |r|))
∨ (b = 0 ∈ (ℕ3 ⟶ |r|))
∨ (∃i:ℕ3. ((¬((b i) = 0 ∈ |r|)) ∧ (¬((a i) = 0 ∈ |r|)) ∧ ((b i*a) = (a i*b) ∈ (ℕ3 ⟶ |r|))))))
Lemma: cross-product-equal-0
∀r:IntegDom{i}. ∀a,b:ℕ3 ⟶ |r|.
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ ((a x b) = 0 ∈ (ℕ3 ⟶ |r|)
⇐⇒ (a = 0 ∈ (ℕ3 ⟶ |r|))
∨ (b = 0 ∈ (ℕ3 ⟶ |r|))
∨ (∃c1,c2:|r|. ((¬(c1 = 0 ∈ |r|)) ∧ (¬(c2 = 0 ∈ |r|)) ∧ ((c1*a) = (c2*b) ∈ (ℕ3 ⟶ |r|))))))
Definition: scalar-product
(a . b) == Σ(r) 0 ≤ i < n. (a i) * (b i)
Lemma: scalar-product_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[a,b:ℕn ⟶ |r|]. ((a . b) ∈ |r|)
Lemma: scalar-product-comm
∀[r:CRng]. ∀[n:ℕ]. ∀[a,b:ℕn ⟶ |r|]. ((a . b) = (b . a) ∈ |r|)
Lemma: scalar-product-0
∀[r:Rng]. ∀[n:ℕ]. ∀[a:ℕn ⟶ |r|]. ((0 . a) = 0 ∈ |r|)
Lemma: scalar-product-mul
∀[r:Rng]. ∀[n:ℕ]. ∀[a,b:ℕn ⟶ |r|]. ∀[c:|r|]. (((c*a) . b) = (c * (a . b)) ∈ |r|)
Lemma: scalar-product-add-left
∀[r:Rng]. ∀[n:ℕ]. ∀[a,b,c:ℕn ⟶ |r|]. (((a + b) . c) = ((a . c) +r (b . c)) ∈ |r|)
Lemma: scalar-product-add-right
∀[r:Rng]. ∀[n:ℕ]. ∀[a,b,c:ℕn ⟶ |r|]. ((c . (a + b)) = ((c . a) +r (c . b)) ∈ |r|)
Definition: scalar-triple-product
|a,b,c| == (a . (b x c))
Lemma: scalar-triple-product_wf
∀[r:Rng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (|a,b,c| ∈ |r|)
Lemma: scalar-product-3
∀[r,a,b:Top]. ((a . b) ~ ((0 +r ((a 0) * (b 0))) +r ((a 1) * (b 1))) +r ((a 2) * (b 2)))
Lemma: Binet-Cauchy-identity
∀[r:CRng]. ∀[a,b,c,d:ℕ3 ⟶ |r|]. (((a x b) . (c x d)) = (((a . c) * (b . d)) +r (-r ((a . d) * (b . c)))) ∈ |r|)
Lemma: Binet-Cauchy-corollary
∀[r:CRng]. ∀[a,b:ℕ3 ⟶ |r|]. (((a x b) . (a x b)) = (((a . a) * (b . b)) +r (-r ((a . b) * (b . a)))) ∈ |r|)
Lemma: non-zero-vector-implies
∀r:RngSig
((∀x,y:|r|. Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. ∀a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} . (∃i:ℕk [(¬((a i) = 0 ∈ |r|))])))
Lemma: non-zero-vector-implies-ext
∀r:RngSig
((∀x,y:|r|. Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. ∀a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} . (∃i:ℕk [(¬((a i) = 0 ∈ |r|))])))
Definition: non-zero-component
non-zero-component(r;eq;k;a) ==
(λr,eq,k,a. eval j' = k in
case letrec G(x)=if (x) < (j')
then if eq (a x) 0 then G (x + 1) else inl <x, λ_.Ax> fi
else (inr (λx.Ax) ) in
G(0)
of inl(p) =>
let i,_ = p
in i
| inr(_) =>
⊥)
r
eq
k
a
Lemma: non-zero-component_wf
∀[r:RngSig]. ∀[eq:∀x,y:|r|. Dec(x = y ∈ |r|)]. ∀[k:ℕ]. ∀[a:{a:ℕk ⟶ |r|| ¬(a = 0 ∈ (ℕk ⟶ |r|))} ].
(non-zero-component(r;eq;k;a) ∈ {i:ℕk| ¬((a i) = 0 ∈ |r|)} )
Lemma: non-zero-component-exists
∀r:RngSig
((∀x,y:|r|. Dec(x = y ∈ |r|)) ⇒ (∀k:ℕ. {∀a:ℕk ⟶ |r|. ((¬(a = 0 ∈ (ℕk ⟶ |r|))) ⇒ (∃i:ℕk. (¬((a i) = 0 ∈ |r|))))}))
Definition: nonzero-cross-imp
nonzero-cross-imp(r;eq;a;b) ==
case int_seg_decide(λi.if eq (a i) 0 then inr (λ%.let %4,%5 = % in Ax)
if eq (b i) 0 then inr (λ%.let %5,%6 = % in Ax)
else inl <λ%.Ax, λ%.Ax>
fi ;0;3)
of inl(tr) =>
let i,pr = tr
in eval i@0 = i in
let _,_ = pr
in if eq (a i@0) 0 then Ax
if int_seg_decide(λx.if eq (* (b i@0) (a x)) (* (a i@0) (b x)) then inr (λ%.Ax) else inl Ax fi ;0;3)
then case int_seg_decide(λj.if eq (* (b i@0) (a j)) (* (a i@0) (b j))
then inr (λ%.Ax)
else inl (λ%.Ax)
fi ;0;3)
of inl(x) =>
let j,_ = x
in λx.if x=i@0 then a j else if x=j then -r (a i@0) else 0
| inr(x) =>
let j,_ = Ax
in λx.if x=i@0 then a j else if x=j then -r (a i@0) else 0
else Ax
fi
| inr(_) =>
λi.if i=non-zero-component(r;eq;3;b) then 1 else 0
Lemma: cross-product-non-zero-implies
∀r:IntegDom{i}
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ (∀a:{a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} . ∀b:{b:ℕ3 ⟶ |r||
(¬(b = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))} .
(∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} [(((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|)))])))
Lemma: cross-product-non-zero-implies-ext
∀r:IntegDom{i}
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ (∀a:{a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} . ∀b:{b:ℕ3 ⟶ |r||
(¬(b = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))} .
(∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} [(((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|)))])))
Lemma: nonzero-cross-imp_wf
∀[r:IntegDom{i}]. ∀[eq:∀x,y:|r|. Dec(x = y ∈ |r|)]. ∀[a:{a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} ]. ∀[b:{b:ℕ3 ⟶ |r||
(¬(b
= 0
∈ (ℕ3 ⟶ |r|)))
∧ (¬((a x b)
= 0
∈ (ℕ3
⟶ |r|)))} ].
(nonzero-cross-imp(r;eq;a;b) ∈ {l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} | ((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|))\000C} )
Lemma: cross-product-equal-0-iff
∀r:IntegDom{i}. ∀a,b:ℕ3 ⟶ |r|.
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ ((a x b) = 0 ∈ (ℕ3 ⟶ |r|)
⇐⇒ (a = 0 ∈ (ℕ3 ⟶ |r|)) ∨ (b = 0 ∈ (ℕ3 ⟶ |r|)) ∨ (∀l:ℕ3 ⟶ |r|. ((a . l) = 0 ∈ |r| ⇐⇒ (b . l) = 0 ∈ |r|))))
Lemma: triple-cross-product-zero
∀r:CRng. ∀a,p,q:ℕ3 ⟶ |r|. (((p . a) = 0 ∈ |r|) ⇒ ((q . a) = 0 ∈ |r|) ⇒ ((a x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|)))
Definition: dual-plane-primitives
DualPlanePrimitives == "V":Type"S":self."V" ⟶ self."V" ⟶ ℙ"P":self."V" ⟶ self."V" ⟶ ℙ
Lemma: dual-plane-primitives_wf
DualPlanePrimitives ∈ 𝕌'
Definition: dp-vec
Vec == d."V"
Lemma: dp-vec_wf
∀[d:DualPlanePrimitives]. (Vec ∈ Type)
Definition: dp-sep
(x # y) == d."S" x y
Lemma: dp-sep_wf
∀[d:DualPlanePrimitives]. ∀[x,y:Vec]. ((x # y) ∈ ℙ)
Definition: dp-perp
(x ⊥ y) == d."P" x y
Lemma: dp-perp_wf
∀[d:DualPlanePrimitives]. ∀[x,y:Vec]. ((x ⊥ y) ∈ ℙ)
Definition: dual-plane-structure
DualPlaneStructure ==
DualPlanePrimitives
"Ssquashstable":∀x,y:Vec. SqStable((x # y))
"Pstable":∀x,y:Vec. Stable{(x ⊥ y)}
"SepOr":∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec. ((z # x) ∨ (z # y))
"cross":∀a:Vec. ∀b:{b:Vec| (a # b)} . (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
"nontrivial":∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])
Lemma: dual-plane-structure_wf
DualPlaneStructure ∈ 𝕌'
Lemma: dual-plane-structure_subtype
DualPlaneStructure ⊆r DualPlanePrimitives
Definition: mk-dp-prim
(vec=V, sep=S, perp=P) == λx.x["V" := V]["S" := S]["P" := P]
Lemma: mk-dp-prim_wf
∀[V:Type]. ∀[S,P:V ⟶ V ⟶ ℙ]. ((vec=V, sep=S, perp=P) ∈ DualPlanePrimitives)
Definition: mk-dp
mk-dp(p;sqs;st;sor;crs;nt) ==
p["Ssquashstable" := sqs]["Pstable" := st]["SepOr" := sor]["cross" := crs]["nontrivial" := nt]
Lemma: mk-dp_wf
∀[self:DualPlanePrimitives]. ∀[sqs:∀x,y:Vec. SqStable((x # y))]. ∀[st:∀x,y:Vec. Stable{(x ⊥ y)}].
∀[sor:∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec. ((z # x) ∨ (z # y))]. ∀[crs:∀a:Vec. ∀b:{b:Vec| (a # b)} .
(∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])].
∀[nt:∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])].
(mk-dp(self;sqs;st;sor;crs;nt) ∈ DualPlaneStructure)
Definition: row-list-matrix
row-list-matrix(L) == matrix(L[x][y])
Lemma: row-list-matrix_wf
∀[n,m:ℕ]. ∀[r:RngSig]. ∀[L:|r| List List].
(row-list-matrix(L) ∈ Matrix(n;m;r)) supposing ((∀i:ℕn. (m ≤ ||L[i]||)) and (n ≤ ||L||))
Lemma: scalar-triple-product-symmetry
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (|a,b,c| = |b,c,a| ∈ |r|)
Lemma: scalar-triple-product-as-det
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|]. (|a,b,c| = |λi.[a; b; c][i]| ∈ |r|)
Lemma: scalar-triple-product-non-zero
∀[r:IntegDom{i}]. ∀[a,b,c:ℕ3 ⟶ |r|].
∀[u:ℕ3 ⟶ |r|]. (((a . u) = 0 ∈ |r|) ⇒ ((b . u) = 0 ∈ |r|) ⇒ ((c . u) = 0 ∈ |r|) ⇒ (u = 0 ∈ (ℕ3 ⟶ |r|)))
supposing ¬(|a,b,c| = 0 ∈ |r|)
Definition: Chio-condensation
Chio-condensation(r;n;A) == matrix((A[i,j] * A[n - 1,n - 1]) +r (-r (A[i,n - 1] * A[n - 1,j])))
Lemma: Chio-condensation_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. (Chio-condensation(r;n;A) ∈ Matrix(n - 1;n - 1;r))
Lemma: rng_lsum-partial-permutations
∀[r:CRng]. ∀[n:{2...}]. ∀[i:ℕn]. ∀[F:(ℕn ⟶ ℕn) ⟶ |r|].
(Σ{r} p ∈ partial-permutations-list(n;i). F[p]
= Σ{r} f ∈ permutations-list(n - 1). F[(i, n - 1) o extend-injection(n - 1;f)]
∈ |r|)
Home
Index