:: MATRLIN semantic presentation begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "k" be ($#m1_hidden :::"Nat":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); :: original: :::"Del"::: redefine func :::"Del"::: "(" "M" "," "k" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "D"; end; theorem :: MATRLIN:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: MATRLIN:2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "M1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k1_matrlin :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) "implies" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")))) ")" ")" ))))) ; theorem :: MATRLIN:3 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "m")) "," (Set (Var "D")) "holds" (Bool (Set ($#k1_matrlin :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")))))) ; theorem :: MATRLIN:4 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) )))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"P":::"*>"::: -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Num 1) "," (Set ($#k3_finseq_1 :::"len"::: ) "P") "," "D"; end; begin begin theorem :: MATRLIN:5 (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 "KL1")) "," (Set (Var "KL2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL1"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL2"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL2"))))) "holds" (Bool (Set (Var "KL1")) ($#r1_vectsp_6 :::"="::: ) (Set (Var "KL2"))))))) ; theorem :: MATRLIN: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 "KL1")) "," (Set (Var "KL2")) "," (Set (Var "KL3")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL1"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL2"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL3"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL3")) ")" )))) "holds" (Bool (Set (Var "KL1")) ($#r1_vectsp_6 :::"="::: ) (Set (Set (Var "KL2")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "KL3")))))))) ; theorem :: MATRLIN:7 (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" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "KL1")) "," (Set (Var "KL2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) ) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL1"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL2"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) & (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL2")) ")" )))) "holds" (Bool (Set (Var "KL1")) ($#r1_vectsp_6 :::"="::: ) (Set (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "KL2"))))))))) ; theorem :: MATRLIN:8 (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 "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b2")) "being" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V")) (Bool "ex" (Set (Var "KL")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL")))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL"))) ($#r1_tarski :::"c="::: ) (Set (Var "b2"))) ")" )))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); attr "V" is :::"finite-dimensional"::: means :: MATRLIN:def 1 (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool (Set (Var "A")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" "V")); end; :: deftheorem defines :::"finite-dimensional"::: MATRLIN:def 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")) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v1_matrlin :::"finite-dimensional"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "A")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V")))) ")" ))); registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#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"::: ) ($#v1_matrlin :::"finite-dimensional"::: ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K"; end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); mode :::"OrdBasis"::: "of" "V" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "V" means :: MATRLIN:def 2 (Bool "(" (Bool it "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) it) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" "V") ")" ); end; :: deftheorem defines :::"OrdBasis"::: MATRLIN:def 2 : (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 "b3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V"))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "b3"))) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V"))) ")" ) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V1", "V2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f1", "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"Function":::) "of" "V1" "," "V2" means :: MATRLIN:def 3 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V1" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "f2" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"+"::: MATRLIN:def 3 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_matrlin :::"+"::: ) (Set (Var "f2")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V1", "V2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V1")) "," (Set (Const "V2")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "a" :::"*"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "V1" "," "V2" means :: MATRLIN:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V1" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k4_vectsp_1 :::"*"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"*"::: MATRLIN:def 4 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_matrlin :::"*"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" )))))); theorem :: MATRLIN: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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a"))))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a"))))))))) ; theorem :: MATRLIN: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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a"))))))))) ; theorem :: MATRLIN:11 (Bool "for" (Set (Var "V1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V1")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V1")))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V1" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "p1" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); let "p2" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V1")); func :::"lmlt"::: "(" "p1" "," "p2" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "V1" equals :: MATRLIN:def 5 (Set (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" "V1") ($#k1_finseqop :::".:"::: ) "(" "p1" "," "p2" ")" ); end; :: deftheorem defines :::"lmlt"::: MATRLIN:def 5 : (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 "p1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "holds" (Bool (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V1"))) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))))); theorem :: MATRLIN: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 "p2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p2"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p1")))))))) ; definitionlet "V1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "M" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V1"))) ($#k3_finseq_2 :::"*"::: ) ); func :::"Sum"::: "M" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "V1" means :: MATRLIN:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" "M" ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Sum"::: MATRLIN:def 6 : (Bool "for" (Set (Var "V1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_matrlin :::"Sum"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "M")) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ))) ")" ) ")" ) ")" )))); theorem :: MATRLIN:13 (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 "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V1"))))))) ; theorem :: MATRLIN:14 (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 "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V1")))))))) ; theorem :: MATRLIN:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_matrlin :::"<*"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "x")) ($#k3_pre_poly :::"*>"::: ) ) ($#k2_matrlin :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_matrlin :::"<*"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "x")) ($#k3_pre_poly :::"*>"::: ) ) ($#k2_matrlin :::"*>"::: ) ) ($#k4_matrix_1 :::"@"::: ) )))) ; theorem :: MATRLIN:16 (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 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: MATRLIN:17 (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 "a")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")))) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k4_finseqop :::"*"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "f")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ) ")" ))))))) ; theorem :: MATRLIN:18 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V3")) "," (Set (Var "V2")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V2")) "," (Set (Var "V3")) (Bool "for" (Set (Var "b2")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V2")) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")))) & (Bool (Set (Var "g")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "a")) "," (Set (Var "b2")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "g")) ($#k4_finseqop :::"*"::: ) (Set (Var "b2")) ")" ) ")" ")" )))))))) ; theorem :: MATRLIN:19 (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 "F")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "KL")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "KL")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "KL")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))))))) ; theorem :: MATRLIN: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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) (Bool "for" (Set (Var "KL")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "KL")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL")))))))) ; theorem :: MATRLIN:21 (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 "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "f1")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f1")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")))) ")" )) "holds" (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: MATRLIN:22 (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 "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f1")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool "for" (Set (Var "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f1")) ($#k4_finseqop :::"*"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k4_finseqop :::"*"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))))))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_matrix_1 :::"tabular"::: ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); :: original: :::"^^"::: redefine func "F" :::"^^"::: "G" -> ($#m2_finseq_1 :::"Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n", "m", "k" be ($#m1_hidden :::"Nat":::); let "M1" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "k")) "," (Set (Const "D")); let "M2" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "m")) "," (Set (Const "k")) "," (Set (Const "D")); :: original: :::"^"::: redefine func "M1" :::"^"::: "M2" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set "n" ($#k2_xcmplx_0 :::"+"::: ) "m") "," "k" "," "D"; end; theorem :: MATRLIN:23 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "M1"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" )))))) ; theorem :: MATRLIN:24 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))) "holds" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")))))))) ; theorem :: MATRLIN:25 (Bool "for" (Set (Var "t")) "," (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "t")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "M2")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M2")) "," (Set (Var "n")) ")" )))))) ; theorem :: MATRLIN:26 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")) ")" )))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M2")) "," (Set (Var "i")) ")" ")" )))))))) ; theorem :: MATRLIN:27 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (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 "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k6_matrlin :::"Sum"::: ) (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M2")) ")" )))))))) ; theorem :: MATRLIN:28 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "D")) (Bool "for" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k8_matrlin :::"^"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k7_matrlin :::"^^"::: ) (Set "(" (Set (Var "M2")) ($#k4_matrix_1 :::"@"::: ) ")" ))))))) ; theorem :: MATRLIN: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 "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) "holds" (Bool (Set (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M1")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_matrlin :::"Sum"::: ) (Set "(" (Set (Var "M1")) ($#k7_matrlin :::"^^"::: ) (Set (Var "M2")) ")" )))))) ; theorem :: MATRLIN:30 (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 "P1")) "," (Set (Var "P2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P2"))))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "P1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "P2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "P1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "P2")) ")" )))))) ; theorem :: MATRLIN:31 (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 "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M1")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set "(" (Set (Var "M1")) ($#k7_matrlin :::"^^"::: ) (Set (Var "M2")) ")" ) ")" )))))) ; theorem :: MATRLIN:32 (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 "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V1"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_matrlin :::"Sum"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) ")" )))))) ; theorem :: MATRLIN:33 (Bool "for" (Set (Var "n")) "," (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 "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "d")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set (Var "d")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ")" ) ")" ")" ))) ")" )) "holds" (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V1")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Set (Var "c")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "b")) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "p")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "d")) "," (Set (Var "b")) ")" ")" ))))))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "b1" be ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Const "V")); let "W" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); func "W" :::"|--"::: "b1" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" means :: MATRLIN:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "b1")) & (Bool "ex" (Set (Var "KL")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" "st" (Bool "(" (Bool "W" ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL")))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "b1")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "KL")) ($#k3_funct_2 :::"."::: ) (Set "(" "b1" ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"|--"::: MATRLIN:def 7 : (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 "b1")) "being" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")))) & (Bool "ex" (Set (Var "KL")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "KL")))) & (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "KL"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "KL")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "b1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" ) ")" )) ")" ) ")" )))))); theorem :: MATRLIN:34 (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 "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V2")) "st" (Bool (Bool (Set (Set (Var "v1")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))))) ; theorem :: MATRLIN:35 (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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V1")) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set "(" (Set (Var "v")) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")) ")" ) "," (Set (Var "b1")) ")" ")" ))))))) ; theorem :: MATRLIN:36 (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 "d")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "d")) "," (Set (Var "b1")) ")" ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b1")))))))) ; theorem :: MATRLIN: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 "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 "a")) "," (Set (Var "d")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))))) "holds" (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "b1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")))) ")" ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_matrlin :::"lmlt"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "f")) ($#k4_finseqop :::"*"::: ) (Set (Var "b1")) ")" ) ")" ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ")" )))))))))) ; 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")); func :::"AutMt"::: "(" "f" "," "b1" "," "b2" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRLIN:def 8 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "b1")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "b1"))) "holds" (Bool (Set it ($#k9_pre_poly :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set "(" "b1" ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) "b2")) ")" ) ")" ); end; :: deftheorem defines :::"AutMt"::: MATRLIN:def 8 : (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")) (Bool "for" (Set (Var "b7")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b7")) ($#k9_pre_poly :::"/."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "b1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ")" ) ($#k9_matrlin :::"|--"::: ) (Set (Var "b2")))) ")" ) ")" ) ")" ))))))); theorem :: MATRLIN:38 (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))))) ; theorem :: MATRLIN: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 "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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))))))) ; theorem :: MATRLIN:40 (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 "f1")) "," (Set (Var "f2")) "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 "f1")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f1")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f1")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f2")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))))))) ; theorem :: MATRLIN:41 (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 :::"Function":::) "of" (Set (Var "V1")) "," (Set (Var "V2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V2")) "," (Set (Var "V3")) (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" ($#m1_matrlin :::"OrdBasis"::: ) "of" (Set (Var "V3")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "g")) "," (Set (Var "b2")) "," (Set (Var "b3")) ")" ")" )))))))))) ; theorem :: MATRLIN:42 (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 "f1")) "," (Set (Var "f2")) "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")) "holds" (Bool (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_matrlin :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f1")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f2")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" )))))))) ; theorem :: MATRLIN:43 (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 "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 "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "holds" (Bool (Set ($#k10_matrlin :::"AutMt"::: ) "(" (Set "(" (Set (Var "a")) ($#k4_matrlin :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_matrix_3 :::"*"::: ) (Set "(" ($#k10_matrlin :::"AutMt"::: ) "(" (Set (Var "f")) "," (Set (Var "b1")) "," (Set (Var "b2")) ")" ")" ))))))))) ;