:: MATRIX_6 semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); pred "M1" :::"commutes_with"::: "M2" means :: MATRIX_6:def 1 (Bool (Set "M1" ($#k4_matrix_3 :::"*"::: ) "M2") ($#r1_hidden :::"="::: ) (Set "M2" ($#k4_matrix_3 :::"*"::: ) "M1")); reflexivity (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))))) ; symmetry (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))))) ; end; :: deftheorem defines :::"commutes_with"::: MATRIX_6:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) "iff" (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1")))) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); pred "M1" :::"is_reverse_of"::: "M2" means :: MATRIX_6:def 2 (Bool "(" (Bool (Set "M1" ($#k4_matrix_3 :::"*"::: ) "M2") ($#r1_hidden :::"="::: ) (Set "M2" ($#k4_matrix_3 :::"*"::: ) "M1")) & (Bool (Set "M1" ($#k4_matrix_3 :::"*"::: ) "M2") ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" "K" "," "n" ")" )) ")" ); symmetry (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1")))) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Const "K")) "," (Set (Const "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2")))) & (Bool (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Const "K")) "," (Set (Const "n")) ")" )) ")" )) ; end; :: deftheorem defines :::"is_reverse_of"::: MATRIX_6:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2"))) "iff" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M1")))) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" ) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M1" is :::"invertible"::: means :: MATRIX_6:def 3 (Bool "ex" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K" "st" (Bool "M1" ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2")))); end; :: deftheorem defines :::"invertible"::: MATRIX_6:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) "iff" (Bool "ex" (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Set (Var "M1")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2")))) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); :: original: :::"-"::: redefine func :::"-"::: "M1" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); :: original: :::"+"::: redefine func "M1" :::"+"::: "M2" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); :: original: :::"-"::: redefine func "M1" :::"-"::: "M2" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; :: original: :::"*"::: redefine func "M1" :::"*"::: "M2" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; theorem :: MATRIX_6:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: MATRIX_6:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: MATRIX_6:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_6:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M3"))) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M3"))))))) ; theorem :: MATRIX_6:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M3"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M3"))))))) ; theorem :: MATRIX_6:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_6:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M2")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M3"))) & (Bool (Set (Var "M1")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); assume (Bool (Set (Const "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) ; func "M1" :::"~"::: -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K" means :: MATRIX_6:def 4 (Bool it ($#r2_matrix_6 :::"is_reverse_of"::: ) "M1"); end; :: deftheorem defines :::"~"::: MATRIX_6:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) )) "iff" (Bool (Set (Var "b4")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M1"))) ")" ))))); theorem :: MATRIX_6:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) ")" ))) ; theorem :: MATRIX_6:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )))) ; theorem :: MATRIX_6:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )))) ; theorem :: MATRIX_6:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" ) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )))) ; theorem :: MATRIX_6:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M3")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M3")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M1"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Set (Var "M3")) ($#k5_matrix_1 :::"@"::: ) ))))) ; theorem :: MATRIX_6:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k5_matrix_1 :::"@"::: ) ))))) ; theorem :: MATRIX_6:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "," (Set (Var "M4")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M3")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M1"))) & (Bool (Set (Var "M4")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M3")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M4"))) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))))))) ; theorem :: MATRIX_6:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M2")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "M"))) ")" )))) ; theorem :: MATRIX_6:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")))) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")))) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M1" is :::"symmetric"::: means :: MATRIX_6:def 5 (Bool (Set "M1" ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) "M1"); end; :: deftheorem defines :::"symmetric"::: MATRIX_6:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "M1"))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k12_matrix_1 :::"1."::: ) "(" "K" "," "n" ")" ) -> ($#v2_matrix_6 :::"symmetric"::: ) ; end; theorem :: MATRIX_6:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a")) ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a"))))))) ; theorem :: MATRIX_6:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_6:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) "iff" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) ")" )))) ; theorem :: MATRIX_6:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "M2")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ; theorem :: MATRIX_6:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_6:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#m1_matrix_1 :::"Upper_Triangular_Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K"))) & (Bool (Set (Var "M1")) "is" ($#m1_matrix_1 :::"Lower_Triangular_Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")))) "holds" (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_6:26 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1")) ")" ) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ; theorem :: MATRIX_6:27 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_6:28 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M1" is :::"antisymmetric"::: means :: MATRIX_6:def 6 (Bool (Set "M1" ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) "M1")); end; :: deftheorem defines :::"antisymmetric"::: MATRIX_6:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1")))) ")" )))); theorem :: MATRIX_6:29 (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_6:30 (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_6:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )))) ; theorem :: MATRIX_6:32 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )))) ; theorem :: MATRIX_6:33 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2"))) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )))) ; theorem :: MATRIX_6:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )) "is" ($#v3_matrix_6 :::"antisymmetric"::: ) )))) ; theorem :: MATRIX_6:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) "iff" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ))) ")" )))) ; theorem :: MATRIX_6:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ")" ))) ")" )))) ; theorem :: MATRIX_6:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ")" ))) ")" )))) ; theorem :: MATRIX_6:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M2")) "," (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix_6 :::"is_reverse_of"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M1" is :::"Orthogonal"::: means :: MATRIX_6:def 7 (Bool "(" (Bool "M1" "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set "M1" ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set "M1" ($#k5_matrix_6 :::"~"::: ) )) ")" ); end; :: deftheorem defines :::"Orthogonal"::: MATRIX_6:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) )) ")" ) ")" )))); theorem :: MATRIX_6:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) ")" ) "iff" (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) ")" )))) ; theorem :: MATRIX_6:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" ) "iff" (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) ")" )))) ; theorem :: MATRIX_6:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ; theorem :: MATRIX_6:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ")" ))) ")" )))) ; theorem :: MATRIX_6:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )))) ; theorem :: MATRIX_6:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_6:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_6:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))))) ; theorem :: MATRIX_6:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_6:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Set (Var "M2")) ($#k5_matrix_1 :::"@"::: ) ))))) ; theorem :: MATRIX_6:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M3"))) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set "(" (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M3")) ")" ) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M3")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ")" ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ")" ))) ")" )))) ; theorem :: MATRIX_6:57 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M3"))) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )))) ; theorem :: MATRIX_6:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ))) ; theorem :: MATRIX_6:59 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )))) ;