:: MATRIX_2 semantic presentation begin definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_hidden :::"set"::: ) ; func "(" "n" "," "m" ")" :::"-->"::: "a" -> ($#v1_matrix_1 :::"tabular"::: ) ($#m1_hidden :::"FinSequence":::) equals :: MATRIX_2:def 1 (Set "n" ($#k2_finseq_2 :::"|->"::: ) (Set "(" "m" ($#k2_finseq_2 :::"|->"::: ) "a" ")" )); end; :: deftheorem defines :::"-->"::: MATRIX_2:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "n")) "," (Set (Var "m")) ")" ($#k1_matrix_2 :::"-->"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "m")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n", "m" be ($#m1_hidden :::"Nat":::); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"-->"::: redefine func "(" "n" "," "m" ")" :::"-->"::: "d" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "m" "," "D"; end; theorem :: MATRIX_2:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "n")) "," (Set (Var "m")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a")) ")" )))) "holds" (Bool (Set (Set "(" "(" (Set (Var "n")) "," (Set (Var "m")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: MATRIX_2:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a9")) ")" ) ($#k14_matrix_1 :::"+"::: ) (Set "(" "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "b9")) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set "(" (Set (Var "a9")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b9")) ")" )))))) ; definitionlet "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func "(" "a" "," "b" ")" :::"]["::: "(" "c" "," "d" ")" -> ($#v1_matrix_1 :::"tabular"::: ) ($#m1_hidden :::"FinSequence":::) equals :: MATRIX_2:def 2 (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "c" "," "d" ($#k10_finseq_1 :::"*>"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ); end; :: deftheorem defines :::"]["::: MATRIX_2:def 2 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ))); theorem :: MATRIX_2:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 2) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 2) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: MATRIX_2:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k3_matrix_2 :::"]["::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ))) ")" )) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"a":::"*>"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); :: original: :::"<*"::: redefine func :::"<*":::"p":::"*>"::: -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Num 1) "," "n" "," "D"; end; theorem :: MATRIX_2:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) ))) & (Bool (Set (Set ($#k5_matrix_2 :::"<*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k5_matrix_2 :::"*>"::: ) ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"]["::: redefine func "(" "a" "," "b" ")" :::"]["::: "(" "c" "," "d" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Num 2) "," "D"; end; theorem :: MATRIX_2:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k6_matrix_2 :::"]["::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))) ; 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")); attr "M" is :::"upper_triangular"::: means :: MATRIX_2:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "j")))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))); attr "M" is :::"lower_triangular"::: means :: MATRIX_2:def 4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))); end; :: deftheorem defines :::"upper_triangular"::: MATRIX_2: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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix_2 :::"upper_triangular"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))); :: deftheorem defines :::"lower_triangular"::: MATRIX_2: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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matrix_2 :::"lower_triangular"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v2_matrix_1 :::"diagonal"::: ) -> ($#v1_matrix_2 :::"upper_triangular"::: ) ($#v2_matrix_2 :::"lower_triangular"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v1_matrix_2 :::"upper_triangular"::: ) ($#v2_matrix_2 :::"lower_triangular"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); mode Upper_Triangular_Matrix of "n" "," "K" is ($#v1_matrix_2 :::"upper_triangular"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; mode Lower_Triangular_Matrix of "n" "," "K" is ($#v2_matrix_2 :::"lower_triangular"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; theorem :: MATRIX_2:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "M")) "is" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) "," (Set (Var "D")))))) ; begin theorem :: MATRIX_2:8 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" )))))) ; definitionlet "i" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); func :::"DelCol"::: "(" "M" "," "i" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" means :: MATRIX_2:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "M"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "M" "," (Set (Var "k")) ")" ")" ) "," "i" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"DelCol"::: MATRIX_2:def 5 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ) "," (Set (Var "i")) ")" )) ")" ) ")" ) ")" )))); theorem :: MATRIX_2:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "M1")) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_1 :::"@"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2"))))) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2"))))) ; theorem :: MATRIX_2:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) ")" ))) ; theorem :: MATRIX_2:11 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "M1")) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_1 :::"@"::: ) ))) "holds" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2"))))) ; theorem :: MATRIX_2:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2"))) "iff" (Bool "(" (Bool (Set (Set (Var "M1")) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M2")) ($#k4_matrix_1 :::"@"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")))) ")" ) ")" ))) ; theorem :: MATRIX_2:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) ($#k4_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: MATRIX_2:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) "," (Set (Var "i")) ")" ))))) ; theorem :: MATRIX_2:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M")) ($#k4_matrix_1 :::"@"::: ) ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ))))) ; theorem :: MATRIX_2:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ))))) ; notationlet "K" be ($#l6_algstr_0 :::"Field":::); let "i" be ($#m1_hidden :::"Nat":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); synonym :::"DelLine"::: "(" "M" "," "i" ")" for :::"Del"::: "(" "i" "," "K" ")" ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "i" be ($#m1_hidden :::"Nat":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); cluster (Set ($#k2_finseq_3 :::"DelLine"::: ) "(" "," "M" ")" ) -> ($#v1_matrix_1 :::"tabular"::: ) ; end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "i" be ($#m1_hidden :::"Nat":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); :: original: :::"DelLine"::: redefine func :::"DelLine"::: "(" "M" "," "i" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K"; end; definitionlet "i", "j", "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 :::"Deleting"::: "(" "M" "," "i" "," "j" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "K" equals :: MATRIX_2:def 6 (Set ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" "M" "," "i" ")" ")" ) "," "j" ")" ); end; :: deftheorem defines :::"Deleting"::: MATRIX_2:def 6 : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (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 ($#k9_matrix_2 :::"Deleting"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) ")" ))))); begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"permutational"::: means :: MATRIX_2:def 7 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"permutational"::: MATRIX_2:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_matrix_2 :::"permutational"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ($#m1_hidden :::"set"::: ) ; func :::"len"::: "P" -> ($#m1_hidden :::"Nat":::) means :: MATRIX_2:def 8 (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "P") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s")))) ")" )); end; :: deftheorem defines :::"len"::: MATRIX_2:def 8 : (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_matrix_2 :::"len"::: ) (Set (Var "P")))) "iff" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s")))) ")" )) ")" ))); definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ($#m1_hidden :::"set"::: ) ; :: original: :::"len"::: redefine func :::"len"::: "P" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Element"::: redefine mode :::"Element"::: "of" "P" -> ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k11_matrix_2 :::"len"::: ) "P" ")" ) ")" ); end; theorem :: MATRIX_2:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k11_matrix_2 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Permutations"::: "n" -> ($#m1_hidden :::"set"::: ) means :: MATRIX_2:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" )) ")" )); end; :: deftheorem defines :::"Permutations"::: MATRIX_2:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) ")" )) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k12_matrix_2 :::"Permutations"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_matrix_2 :::"permutational"::: ) ; end; theorem :: MATRIX_2:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k11_matrix_2 :::"len"::: ) (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: MATRIX_2:19 (Bool (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Num 1) ")" ) ($#k1_tarski :::"}"::: ) )) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Group_of_Perm"::: "n" -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: MATRIX_2:def 10 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_2 :::"Permutations"::: ) "n")) & (Bool "(" "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) "n") "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q")))) ")" ) ")" ); end; :: deftheorem defines :::"Group_of_Perm"::: MATRIX_2:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "q")) "," (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b2"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q")))) ")" ) ")" ) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k13_matrix_2 :::"Group_of_Perm"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: MATRIX_2:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" ))) ; theorem :: MATRIX_2:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ))) ; theorem :: MATRIX_2:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")))) ")" ))) ; theorem :: MATRIX_2:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k13_matrix_2 :::"Group_of_Perm"::: ) "n") -> ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ; end; theorem :: MATRIX_2:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n")) ")" ); attr "p" is :::"being_transposition"::: means :: MATRIX_2:def 11 (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" )); end; :: deftheorem defines :::"being_transposition"::: MATRIX_2:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) "iff" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" )) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "IT" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n")) ")" ); attr "IT" is :::"even"::: means :: MATRIX_2:def 12 (Bool "ex" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) "n" ")" ) "st" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "IT" ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "l")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "l"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) "n") "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"even"::: MATRIX_2:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_matrix_2 :::"even"::: ) ) "iff" (Bool "ex" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "l")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "l"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) ")" ) ")" )) ")" ))); notationlet "n" be ($#m1_hidden :::"Nat":::); let "IT" be ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n")) ")" ); antonym :::"odd"::: "IT" for :::"even"::: ; end; theorem :: MATRIX_2:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) "is" ($#v5_matrix_2 :::"even"::: ) )) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "p" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Const "n"))); func :::"-"::: "(" "x" "," "p" ")" -> ($#m1_subset_1 :::"Element":::) "of" "K" equals :: MATRIX_2:def 13 "x" if (Bool "p" "is" ($#v5_matrix_2 :::"even"::: ) ) otherwise (Set ($#k4_algstr_0 :::"-"::: ) "x"); end; :: deftheorem defines :::"-"::: MATRIX_2:def 13 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix_2 :::"even"::: ) )) "implies" (Bool (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) "is" ($#v5_matrix_2 :::"even"::: ) ))) "implies" (Bool (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")))) ")" ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) ; func :::"FinOmega"::: "X" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X") equals :: MATRIX_2:def 14 "X"; end; :: deftheorem defines :::"FinOmega"::: MATRIX_2:def 14 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k15_matrix_2 :::"FinOmega"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))); theorem :: MATRIX_2:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ;