:: MATRIX_8 semantic presentation begin 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 :::"Idempotent"::: means :: MATRIX_8:def 1 (Bool (Set "M1" ($#k4_matrix_6 :::"*"::: ) "M1") ($#r1_hidden :::"="::: ) "M1"); attr "M1" is :::"Nilpotent"::: means :: MATRIX_8:def 2 (Bool (Set "M1" ($#k4_matrix_6 :::"*"::: ) "M1") ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" "K" "," "n" ")" )); attr "M1" is :::"Involutory"::: means :: MATRIX_8:def 3 (Bool (Set "M1" ($#k4_matrix_6 :::"*"::: ) "M1") ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" "K" "," "n" ")" )); attr "M1" is :::"Self_Reversible"::: means :: MATRIX_8:def 4 (Bool "(" (Bool "M1" "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set "M1" ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) "M1") ")" ); end; :: deftheorem defines :::"Idempotent"::: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Var "M1"))) ")" )))); :: deftheorem defines :::"Nilpotent"::: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" )))); :: deftheorem defines :::"Involutory"::: MATRIX_8: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" ($#v3_matrix_8 :::"Involutory"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )) ")" )))); :: deftheorem defines :::"Self_Reversible"::: MATRIX_8: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")) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v4_matrix_8 :::"Self_Reversible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "M1"))) ")" ) ")" )))); theorem :: MATRIX_8:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v3_matrix_8 :::"Involutory"::: ) ) ")" ))) ; theorem :: MATRIX_8:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) ")" ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k12_matrix_1 :::"1."::: ) "(" "K" "," "n" ")" ) -> ($#v1_matrix_8 :::"Idempotent"::: ) ($#v3_matrix_8 :::"Involutory"::: ) ; cluster (Set ($#k11_matrix_1 :::"0."::: ) "(" "K" "," "n" ")" ) -> ($#v1_matrix_8 :::"Idempotent"::: ) ($#v2_matrix_8 :::"Nilpotent"::: ) ; end; theorem :: MATRIX_8: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")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) "iff" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) ")" )))) ; theorem :: MATRIX_8: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" ($#v3_matrix_8 :::"Involutory"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )))) ; theorem :: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (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_8: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")) "," (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" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8: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")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" )))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:8 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:9 (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"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:10 (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"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8:11 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:12 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M2")) ($#k5_matrix_1 :::"@"::: ) ")" )) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:13 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:14 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_8:15 (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 (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 (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8:16 (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_8 :::"Idempotent"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8: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")) "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 (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_8: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")) "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 (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) "is" ($#v2_matrix_6 :::"symmetric"::: ) )))) ; theorem :: MATRIX_8: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")) "," (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 (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M3"))))) "holds" (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set (Var "M3")))))) ; theorem :: MATRIX_8:20 (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 (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M3")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set (Var "M3")))))) ; theorem :: MATRIX_8:21 (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 "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8: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 "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8: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")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )))) ; theorem :: MATRIX_8: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 "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "M1")) ($#r1_matrix_6 :::"commutes_with"::: ) (Set (Var "M2"))) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )))) ; theorem :: MATRIX_8: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")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )))) ; theorem :: MATRIX_8:26 (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" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )))) ; theorem :: MATRIX_8:27 (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" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" )))) ; theorem :: MATRIX_8:29 (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"::: ) )) & (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )) "holds" (Bool "not" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) ))))) ; theorem :: MATRIX_8:30 (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_8 :::"Self_Reversible"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v3_matrix_8 :::"Involutory"::: ) )))) ; theorem :: MATRIX_8:31 (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_8 :::"Self_Reversible"::: ) ))) ; theorem :: MATRIX_8:32 (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_8 :::"Self_Reversible"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ))))) ; theorem :: MATRIX_8:33 (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_8 :::"Self_Reversible"::: ) ) & (Bool (Set (Var "M1")) "is" ($#v2_matrix_6 :::"symmetric"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )))) ; 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_similar_to"::: "M2" means :: MATRIX_8:def 5 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K" "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool "M1" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) "M2" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" )); reflexivity (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" ))) ; symmetry (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" ))) "holds" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" ))) ; end; :: deftheorem defines :::"is_similar_to"::: MATRIX_8: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")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) "iff" (Bool "ex" (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 "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_6 :::"~"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" )) ")" )))); theorem :: MATRIX_8: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")) "," (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_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M3")))) "holds" (Bool (Set (Var "M1")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX_8: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 "M1")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v1_matrix_8 :::"Idempotent"::: ) )))) ; theorem :: MATRIX_8: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")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "M1")) "is" ($#v2_matrix_8 :::"Nilpotent"::: ) )))) ; theorem :: MATRIX_8: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")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) "is" ($#v3_matrix_8 :::"Involutory"::: ) )) "holds" (Bool (Set (Var "M1")) "is" ($#v3_matrix_8 :::"Involutory"::: ) )))) ; theorem :: MATRIX_8: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")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: MATRIX_8:39 (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_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8: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")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Set "(" (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8: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")) "," (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"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8:42 (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 (Var "M1")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )))) ; theorem :: MATRIX_8:43 (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 (Var "M1")) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_6 :::"~"::: ) ) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Set (Var "M2")) ($#k5_matrix_6 :::"~"::: ) ))))) ; 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_congruent_Matrix_of"::: "M2" means :: MATRIX_8:def 6 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K" "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool "M1" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) "M2" ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" )); reflexivity (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")) "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_6 :::"invertible"::: ) ) & (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" ))) ; end; :: deftheorem defines :::"is_congruent_Matrix_of"::: MATRIX_8: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")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) "iff" (Bool "ex" (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 "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M")))) ")" )) ")" )))); theorem :: MATRIX_8: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")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "M2")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M1")))))) ; theorem :: MATRIX_8: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")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M3"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M3")))))) ; theorem :: MATRIX_8: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 "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8: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")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M1"))) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Set "(" (Set (Var "M2")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8: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 "M1")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M1"))) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Set (Var "M1")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2"))))))) ; theorem :: MATRIX_8:49 (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 (Var "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "M1")) "is" ($#v1_matrix_6 :::"invertible"::: ) )))) ; theorem :: MATRIX_8: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 "M1")) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Var "M2"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r2_matrix_8 :::"is_congruent_Matrix_of"::: ) (Set (Set (Var "M2")) ($#k5_matrix_1 :::"@"::: ) ))))) ; theorem :: MATRIX_8:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M4")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M4")) "is" ($#v4_matrix_6 :::"Orthogonal"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "M4")) ($#k5_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M2")) ")" ) ($#k4_matrix_6 :::"*"::: ) (Set (Var "M4"))) ($#r1_matrix_8 :::"is_similar_to"::: ) (Set (Var "M2")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); func :::"Trace"::: "M" -> ($#m1_subset_1 :::"Element":::) "of" "K" equals :: MATRIX_8:def 7 (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k13_matrix_3 :::"diagonal_of_Matrix"::: ) "M" ")" )); end; :: deftheorem defines :::"Trace"::: MATRIX_8: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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k13_matrix_3 :::"diagonal_of_Matrix"::: ) (Set (Var "M")) ")" )))))); theorem :: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ; theorem :: MATRIX_8: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")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" )))))) ; theorem :: MATRIX_8: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")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M3")) ")" )))))) ; theorem :: MATRIX_8:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" ($#k11_matrix_1 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; theorem :: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" )))))) ; theorem :: MATRIX_8: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")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set "(" ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1"))))))) ; theorem :: MATRIX_8:58 (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 ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set "(" ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX_8: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")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" )))))) ; theorem :: MATRIX_8:60 (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")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set "(" (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M3")) ")" )))))) ; theorem :: MATRIX_8:61 (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")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M3")) ")" )))))) ; theorem :: MATRIX_8:62 (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")) "holds" (Bool (Set ($#k1_matrix_8 :::"Trace"::: ) (Set "(" (Set "(" (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_matrix_8 :::"Trace"::: ) (Set (Var "M3")) ")" )))))) ;