:: MATRLIN2 semantic presentation begin theorem :: MATRLIN2:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W12")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W12")) "st" (Bool (Bool (Set (Var "U1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "U2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "U2")))) & (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "U2")))) ")" ))))) ; theorem :: MATRLIN2:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))))) "holds" (Bool "for" (Set (Var "B1")) "being" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W1")) (Bool "for" (Set (Var "B2")) "being" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W2")) "holds" (Bool (Set (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B2"))) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ))))))) ; theorem :: MATRLIN2:3 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))))) "holds" (Bool "for" (Set (Var "B1")) "being" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "W2")) "holds" (Bool (Set (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B2"))) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))))))))) ; theorem :: MATRLIN2:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))) "holds" (Bool (Set (Var "B")) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V")))))) ; theorem :: MATRLIN2:5 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) )))) ; theorem :: MATRLIN2:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))))) ; begin theorem :: MATRLIN2:7 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "R")) ")" ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p2")) "," (Set (Var "R")) ")" ")" ))))))) ; theorem :: MATRLIN2:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "R1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "R1")) ")" ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "R2")) ")" ")" ))))))) ; theorem :: MATRLIN2:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R2"))))) "holds" (Bool (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" (Set (Var "p1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ) "," (Set "(" (Set (Var "R1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "R2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "R1")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p2")) "," (Set (Var "R2")) ")" ")" ))))))) ; theorem :: MATRLIN2:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "R2"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2")) ")" )))))) ; theorem :: MATRLIN2:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) "," (Set (Var "R")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R")) ")" ))))))) ; theorem :: MATRLIN2:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "v1")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")))))))) ; theorem :: MATRLIN2:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "R")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "R")) ")" ")" ) ")" )))))))) ; theorem :: MATRLIN2:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "B1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "W1")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "B1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "B2")) ")" )))))))) ; theorem :: MATRLIN2:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "B1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "W1")) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "B2"))))))))) ; theorem :: MATRLIN2:16 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) ")" ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "R")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))))))) ; begin theorem :: MATRLIN2:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v1")) "," (Set (Var "w1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Set "(" (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "w1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ))))))) ; theorem :: MATRLIN2:18 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" )))))))) ; theorem :: MATRLIN2:19 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")) ")" ) ")" ")" ) "," (Set (Var "i")) ")" )))))) ; theorem :: MATRLIN2:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; theorem :: MATRLIN2:21 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V1"))))))) ; theorem :: MATRLIN2:22 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "b1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "m")) ")" )) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "b1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "m")) ")" )))) "holds" (Bool (Set (Set (Var "b1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "m"))) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")))) ")" ) ")" ))))) ; theorem :: MATRLIN2:23 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "b1")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "m")) ")" )) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1"))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "b1")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "m")) ")" )))) "holds" (Bool (Set (Set (Var "b1")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "m"))) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")))) ")" ) ")" ))))) ; theorem :: MATRLIN2:24 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V1"))))) "holds" (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W2")) (Bool "for" (Set (Var "b")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "b2"))))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) (Bool "for" (Set (Var "w1")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W1")) (Bool "for" (Set (Var "w2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W2")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Set (Var "v")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "w1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "w2")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")) ")" )))))))))))) ; theorem :: MATRLIN2:25 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V1"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W1")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "w1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W1")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "w1")))) "holds" (Bool (Set (Set (Var "v")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k9_matrlin :::"|--"::: ) (Set (Var "w1"))))))))))) ; theorem :: MATRLIN2:26 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V1"))))) "holds" (Bool "for" (Set (Var "w1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "w2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W2")) "holds" (Bool (Set (Set (Var "w1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "w2"))) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))))))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); let "B1" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V1")); let "b2" be ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Const "V2")); :: original: :::"AutMt"::: redefine func :::"AutMt"::: "(" "f" "," "B1" "," "b2" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "B1") "," (Set ($#k3_finseq_1 :::"len"::: ) "b2") "," "K"; end; definitionlet "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); func "R" :::"|"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: MATRLIN2:def 1 (Set "R" ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")); end; :: deftheorem defines :::"|"::: MATRLIN2:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k2_matrlin2 :::"|"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))))); theorem :: MATRLIN2:27 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V2")) "st" (Bool "(" (Bool (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "U1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" & "(" (Bool (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "U2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" & (Bool (Set (Var "V2")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "U1")) "," (Set (Var "U2")))) "holds" (Bool "for" (Set (Var "fW1")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "W1")) "," (Set (Var "U1")) (Bool "for" (Set (Var "fW2")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "W2")) "," (Set (Var "U2")) "st" (Bool (Bool (Set (Var "fW1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_matrlin2 :::"|"::: ) (Set (Var "W1")))) & (Bool (Set (Var "fW2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_matrlin2 :::"|"::: ) (Set (Var "W2"))))) "holds" (Bool "for" (Set (Var "w1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "w2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "W2")) (Bool "for" (Set (Var "u1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "U1")) (Bool "for" (Set (Var "u2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "U2")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Set (Var "u1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "u2"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set "(" ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "fW1")) "," (Set (Var "w1")) "," (Set (Var "u1")) ")" ")" ) "," (Set "(" ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "fW2")) "," (Set (Var "w2")) "," (Set (Var "u2")) ")" ")" ) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ))))))))))))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); let "B1" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V1")); let "b2" be ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Const "V2")); assume (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "b2")))) ; func :::"AutEqMt"::: "(" "f" "," "B1" "," "b2" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "B1") "," (Set ($#k3_finseq_1 :::"len"::: ) "B1") "," "K" equals :: MATRLIN2:def 2 (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" "f" "," "B1" "," "b2" ")" ); end; :: deftheorem defines :::"AutEqMt"::: MATRLIN2:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "B1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k3_matrlin2 :::"AutEqMt"::: ) "(" (Set (Var "f")) "," (Set (Var "B1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "B1")) "," (Set (Var "b2")) ")" ))))))); theorem :: MATRLIN2:28 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "V1")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")) ")" ) ")" ))))) ; theorem :: MATRLIN2:29 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b19")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "holds" (Bool "(" (Bool (Set ($#k3_matrlin2 :::"AutEqMt"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "V1")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b19")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set ($#k3_matrlin2 :::"AutEqMt"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "V1")) ")" ) "," (Set (Var "b19")) "," (Set (Var "b1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_matrlin2 :::"AutEqMt"::: ) "(" (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "V1")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b19")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) )) ")" )))) ; theorem :: MATRLIN2:30 (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p2"))))) "holds" (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "B1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" )) "holds" (Bool (Set (Set (Var "p1")) ($#k13_fvsum_1 :::""*""::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "B1")) ")" ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))))))))) ; theorem :: MATRLIN2:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V2")) "," (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")) ")" ))))))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "b1" be ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Const "V1")); let "B2" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V2")); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "B2"))) "," (Set (Const "K")); func :::"Mx2Tran"::: "(" "M" "," "b1" "," "B2" ")" -> ($#m1_subset_1 :::"Function":::) "of" "V1" "," "V2" means :: MATRLIN2:def 3 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V1" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "v")) ($#k9_matrlin :::"|--"::: ) "b1" ")" ) ")" ) ($#k4_matrix_3 :::"*"::: ) "M" ")" ) "," (Num 1) ")" ")" ) "," "B2" ")" ")" )))); end; :: deftheorem defines :::"Mx2Tran"::: MATRLIN2:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2"))) "," (Set (Var "K")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" )) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Set (Var "b7")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "v")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M")) ")" ) "," (Num 1) ")" ")" ) "," (Set (Var "B2")) ")" ")" )))) ")" ))))))); theorem :: MATRLIN2:32 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V2")) "," (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set "(" (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M")))))))))) ; theorem :: MATRLIN2:33 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V2")))))))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "b1" be ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Const "V1")); let "B2" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V2")); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "B2"))) "," (Set (Const "K")); cluster (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" "M" "," "b1" "," "B2" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_2 :::"homogeneous"::: ) ; end; theorem :: MATRLIN2:34 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set "(" ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))))) ; theorem :: MATRLIN2:35 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix15 :::"LineVec2Mx"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" ")" )))))) ; theorem :: MATRLIN2:36 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "M")))))))) ; definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "A" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "K")); let "B" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); :: original: :::"+"::: redefine func "A" :::"+"::: "B" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "m" "," "K"; end; theorem :: MATRLIN2:37 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2"))) "," (Set (Var "K")) "holds" (Bool (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set "(" (Set (Var "A")) ($#k5_matrlin2 :::"+"::: ) (Set (Var "B")) ")" ) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" ")" ) ($#k3_matrlin :::"+"::: ) (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "B")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" ")" )))))))) ; theorem :: MATRLIN2:38 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "B2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V2")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2"))) "," (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k4_matrlin :::"*"::: ) (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "A")) ")" ) "," (Set (Var "b1")) "," (Set (Var "B2")) ")" )))))))) ; theorem :: MATRLIN2:39 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "B")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))))))) ; theorem :: MATRLIN2:40 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "V3")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "B3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V3")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) (Bool "for" (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B3"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))))) "holds" (Bool "for" (Set (Var "AB")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B3"))) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "AB")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "AB")) "," (Set (Var "b1")) "," (Set (Var "B3")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "B")) "," (Set (Var "b2")) "," (Set (Var "B3")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ))))))))))) ; theorem :: MATRLIN2:41 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V2")) "," (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_ranknull :::"ker"::: ) (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ))) "iff" (Bool (Set (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k7_matrix15 :::"Space_of_Solutions_of"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_1 :::"@"::: ) ")" ))) ")" ))))))) ; theorem :: MATRLIN2:42 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v7_struct_0 :::"trivial"::: ) ) "iff" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ))) ; theorem :: MATRLIN2:43 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V1")))) ")" )))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f", "g" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); cluster (Set "f" ($#k3_matrlin :::"+"::: ) "g") -> ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_2 :::"homogeneous"::: ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k4_matrlin :::"*"::: ) "f") -> ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_2 :::"homogeneous"::: ) ; end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2", "V3" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f1" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); let "f2" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V2")) "," (Set (Const "V3")); :: original: :::"(#)"::: redefine func "f2" :::"*"::: "f1" -> ($#m1_subset_1 :::"linear-transformation":::) "of" "V1" "," "V3"; end; theorem :: MATRLIN2:44 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))))) "holds" (Bool (Set ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))))) ; theorem :: MATRLIN2:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k11_matrix13 :::"MX2FinS"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Set (Var "n")) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K")))))) ; theorem :: MATRLIN2:46 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix13 :::"MX2FinS"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ")" )))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K")) ")" ) "holds" (Bool (Set (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "v1")))))))) ; theorem :: MATRLIN2:47 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V2")) "," (Set (Var "V1")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k6_prvect_1 :::"-VectSp_over"::: ) (Set (Var "K"))) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix13 :::"MX2FinS"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ")" ")" )))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" )) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "A")) "," (Set (Var "b1")) "," (Set (Var "M")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")))))))))))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V1", "V2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V1")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); :: original: :::"|"::: redefine func "f" :::"|"::: "W" -> ($#m1_subset_1 :::"Function":::) "of" "W" "," "V2"; end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1", "V2" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V1")); let "f" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); :: original: :::"|"::: redefine func "f" :::"|"::: "W" -> ($#m1_subset_1 :::"linear-transformation":::) "of" "W" "," "V2"; end; begin theorem :: MATRLIN2:48 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "holds" (Bool (Set ($#k10_ranknull :::"rank"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set "(" ($#k1_matrlin2 :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )))))))) ; theorem :: MATRLIN2:49 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) "," (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "," (Set (Var "K")) "holds" (Bool (Set ($#k10_ranknull :::"rank"::: ) (Set "(" ($#k4_matrlin2 :::"Mx2Tran"::: ) "(" (Set (Var "M")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix13 :::"the_rank_of"::: ) (Set (Var "M"))))))))) ; theorem :: MATRLIN2:50 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "st" (Bool (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V2"))))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "f"))) "is" ($#v7_struct_0 :::"trivial"::: ) )) "iff" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrlin2 :::"AutEqMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" )))))) ; theorem :: MATRLIN2:51 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "V3")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V2")) "," (Set (Var "V3")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k8_matrlin2 :::"|"::: ) (Set "(" ($#k3_ranknull :::"im"::: ) (Set (Var "f")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set ($#k10_ranknull :::"rank"::: ) (Set "(" (Set (Var "g")) ($#k6_matrlin2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_ranknull :::"rank"::: ) (Set (Var "f")))) & (Bool (Set ($#k11_ranknull :::"nullity"::: ) (Set "(" (Set (Var "g")) ($#k6_matrlin2 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_ranknull :::"nullity"::: ) (Set (Var "f")))) ")" ))))) ;