:: MATRIX11 semantic presentation begin notationlet "X" be ($#m1_hidden :::"set"::: ) ; synonym :::"2Set"::: "X" for :::"TWOELEMENTSETS"::: "X"; end; theorem :: MATRIX11:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ))) "iff" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" ))) ; theorem :: MATRIX11:2 (Bool "(" (Bool (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: MATRIX11:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "perm" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Const "n"))); cluster (Set "perm" ($#k1_funct_1 :::"."::: ) "x") -> ($#v7_ordinal1 :::"natural"::: ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") -> ($#v1_setwiseo :::"having_a_unity"::: ) ; cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") -> ($#v2_binop_1 :::"associative"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "perm2" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Const "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )); func :::"Part_sgn"::: "(" "perm2" "," "K" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") means :: MATRIX11:def 1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "(" "(" (Bool (Bool (Set "perm2" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set "perm2" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "K")) ")" & "(" (Bool (Bool (Set "perm2" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set "perm2" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "K" ")" ))) ")" ")" )); end; :: deftheorem defines :::"Part_sgn"::: MATRIX11: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 "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" )) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "perm2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "perm2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Set (Var "perm2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "perm2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ")" )) ")" ))))); theorem :: MATRIX11:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) ")" )) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))))))) ; theorem :: MATRIX11:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) "or" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ))))) ; theorem :: MATRIX11:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ))))))) ; theorem :: MATRIX11:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" )) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "F")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) ")" ) "}" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ")" ) ")" ")" ))) ")" ")" )))))) ; theorem :: MATRIX11:8 (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")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "iff" (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 (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"))) ")" ) ")" ) ")" )))) ; theorem :: MATRIX11:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "pq2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "pq2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q2")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) & (Bool (Set (Set (Var "q2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) "holds" (Bool "(" "not" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) "or" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) "or" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" )))))) ; theorem :: MATRIX11:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "pq2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "pq2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q2")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) & (Bool (Set (Set (Var "q2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "k")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "k")) ($#k2_tarski :::"}"::: ) ))) "iff" (Bool (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "j")) "," (Set (Var "k")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "j")) "," (Set (Var "k")) ($#k2_tarski :::"}"::: ) ))) ")" ) ")" ) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "perm2" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Const "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )); func :::"sgn"::: "(" "perm2" "," "K" ")" -> ($#m1_subset_1 :::"Element":::) "of" "K" equals :: MATRIX11:def 2 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" "perm2" "," "K" ")" ")" ) ")" ); end; :: deftheorem defines :::"sgn"::: MATRIX11: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 "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k2_sgraph1 :::"2Set"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) "," (Set "(" ($#k1_matrix11 :::"Part_sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ")" ) ")" ))))); theorem :: MATRIX11:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) "or" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" )))) ; theorem :: MATRIX11:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "Id")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "Id")) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_2 :::"idseq"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )))) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "Id")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K"))))))) ; theorem :: MATRIX11:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "pq2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "pq2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q2")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" )))))) ; theorem :: MATRIX11:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "tr")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" )))))) ; theorem :: MATRIX11:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "P")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) (Bool "for" (Set (Var "p2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "P")))) & (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 "P"))))) "holds" (Bool "ex" (Set (Var "trans")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "trans"))) & (Bool (Set (Var "trans")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "implies" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "P")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" ")" ))))) ; theorem :: MATRIX11:16 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) & (Bool (Set (Set (Var "tr")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) ")" ))) ; theorem :: MATRIX11:17 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) "st" (Bool "(" (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) & (Bool (Set (Set (Var "tr")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "tr")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1))) ")" )))) ; theorem :: MATRIX11:18 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Set (Set (Var "p1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))) ; theorem :: MATRIX11:19 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "q1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "q1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p1")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q1")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q")))) & (Bool (Set (Set "(" (Set (Var "p1")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: MATRIX11:20 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "k"))) "st" (Bool (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "tr")) ($#k1_partfun1 :::"*"::: ) (Set (Var "tr"))) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "k")))) & (Bool (Set (Var "tr")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "tr")) ($#k2_funct_2 :::"""::: ) )) ")" ))) ; theorem :: MATRIX11:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "P")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "perm")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "P")))) & (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 "P"))))) "holds" (Bool "ex" (Set (Var "trans")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "trans"))) & (Bool (Set (Var "trans")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) ")" ) ")" )))) ; theorem :: MATRIX11:22 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v12_vectsp_1 :::"Fanoian"::: ) ) "iff" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" )) ; theorem :: MATRIX11:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "perm2")) "is" ($#v5_matrix_2 :::"even"::: ) )) "implies" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) ")" & "(" (Bool (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K"))))) "implies" (Bool (Set (Var "perm2")) "is" ($#v5_matrix_2 :::"even"::: ) ) ")" & "(" (Bool (Bool (Set (Var "perm2")) "is" ($#v5_matrix_2 :::"odd"::: ) )) "implies" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ))) ")" & "(" (Bool (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" )))) "implies" (Bool (Set (Var "perm2")) "is" ($#v5_matrix_2 :::"odd"::: ) ) ")" ")" )))) ; theorem :: MATRIX11:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "," (Set (Var "pq2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "pq2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q2"))))) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "pq2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ")" )))))) ; theorem :: MATRIX11:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v5_matrix_2 :::"even"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix_2 :::"even"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) "is" ($#v5_matrix_2 :::"odd"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix_2 :::"odd"::: ) ) ")" ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "q"))) "is" ($#v5_matrix_2 :::"even"::: ) ) ")" ))) ; theorem :: MATRIX11:26 (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")) (Bool "for" (Set (Var "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "holds" (Bool (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set (Var "a")) "," (Set (Var "perm2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a")))))))) ; theorem :: MATRIX11:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool (Set (Var "tr")) "is" ($#v5_matrix_2 :::"odd"::: ) ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_funct_2 :::"onto"::: ) ($#v3_funct_2 :::"bijective"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v5_matrix_2 :::"odd"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; begin definitionlet "l", "n", "m" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "D")); let "pD" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); func :::"ReplaceLine"::: "(" "M" "," "l" "," "pD" ")" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "m" "," "D" means :: MATRIX11:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (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"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) "l")) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" "l" "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "pD" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ")" ) ")" ) ")" ) if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "pD") ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) otherwise (Bool it ($#r1_hidden :::"="::: ) "M"); end; :: deftheorem defines :::"ReplaceLine"::: MATRIX11:def 3 : (Bool "for" (Set (Var "l")) "," (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 "pD")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b7")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pD"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "implies" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix11 :::"ReplaceLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pD")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (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"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "l")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "pD")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ")" ) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pD"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))))) "implies" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix11 :::"ReplaceLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pD")) ")" )) "iff" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Var "M"))) ")" ) ")" ")" )))))); notationlet "l", "n", "m" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "D")); let "pD" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); synonym :::"RLine"::: "(" "M" "," "l" "," "pD" ")" for :::"ReplaceLine"::: "(" "M" "," "l" "," "pD" ")" ; end; theorem :: MATRIX11:28 (Bool "for" (Set (Var "m")) "," (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 "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "pD")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "l"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pD"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pD")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "pD"))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pD")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" )) ")" ")" ))))))) ; theorem :: MATRIX11:29 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "l")) "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 "pD")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pD"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "p9")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "pD")) ($#r1_hidden :::"="::: ) (Set (Var "p9")))) "holds" (Bool (Set ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pD")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_finseq_7 :::"Replace"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "p9")) ")" ))))))) ; theorem :: MATRIX11:30 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "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")) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) ")" ")" ) ")" ))))) ; theorem :: MATRIX11:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "pK")) "," (Set (Var "qK")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pK"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qK"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "perm")) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "pK")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "qK")) ")" ) ")" ) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "perm")) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pK")) ")" ")" ) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "perm")) "," (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "qK")) ")" ")" ) ")" ")" ) ")" ) ")" )))))))))) ; theorem :: MATRIX11:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "pK")) "," (Set (Var "qK")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pK"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qK"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "pK")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "qK")) ")" ) ")" ) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "perm"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pK")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "perm")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "qK")) ")" ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "perm")) ")" ) ")" )))))))))) ; theorem :: MATRIX11:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "pK")) "," (Set (Var "qK")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pK"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qK"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "pK")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "qK")) ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "pK")) ")" ")" ) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "M")) "," (Set (Var "l")) "," (Set (Var "qK")) ")" ")" ) ")" ) ")" ))))))))) ; theorem :: MATRIX11:34 (Bool "for" (Set (Var "l")) "," (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")) (Bool "for" (Set (Var "pK")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pK"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "pK")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "pK")) ")" ")" ) ")" )))))))) ; theorem :: MATRIX11:35 (Bool "for" (Set (Var "l")) "," (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")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) ")" ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: MATRIX11:36 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "pK")) "," (Set (Var "qK")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pK"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qK"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set "(" (Set (Var "pK")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "qK")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "pK")) ")" ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "l")) "," (Set (Var "qK")) ")" ")" ) ")" ))))))) ; begin definitionlet "n", "m" be ($#m1_hidden :::"Nat":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Const "n")) ")" ); let "M" be ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set (Const "D")); :: original: :::"*"::: redefine func "M" :::"*"::: "F" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "m" "," "D" means :: MATRIX11:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "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 "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"*"::: MATRIX11:def 4 : (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "M")) "," (Set (Var "b6")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "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 (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "b6")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) ")" ) ")" ) ")" ))))); theorem :: MATRIX11:37 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")) ")" ))) & (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"))))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "j")) ")" )) ")" )) ")" ) ")" ))))) ; theorem :: MATRIX11:38 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (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 ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" )))))))) ; theorem :: MATRIX11:39 (Bool "for" (Set (Var "m")) "," (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" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "M")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: MATRIX11:40 (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_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "Perm")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "Perm")) ($#k2_funct_2 :::"""::: ) ")" )))) "holds" (Bool (Set ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "A")) ($#k4_matrix11 :::"*"::: ) (Set (Var "Perm")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "q")) "," (Set (Var "A")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "Perm")))))))))) ; theorem :: MATRIX11:41 (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_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "Perm")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "Perm")) ($#k2_funct_2 :::"""::: ) ")" )))) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "A")) ($#k4_matrix11 :::"*"::: ) (Set (Var "Perm")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "q")) "," (Set (Var "A")) ")" ")" ))))))))) ; theorem :: MATRIX11:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "q2")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k2_funct_2 :::"""::: ) ))) "holds" (Bool (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "p2")) "," (Set (Var "K")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "q2")) "," (Set (Var "K")) ")" ))))) ; theorem :: MATRIX11:43 (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 (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) "," (Set (Var "K")) (Bool "for" (Set (Var "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "Perm2")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "st" (Bool (Bool (Set (Var "perm2")) ($#r1_hidden :::"="::: ) (Set (Var "Perm2")))) "holds" (Bool "for" (Set (Var "p2")) "," (Set (Var "q2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "q2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "Perm2")) ($#k2_funct_2 :::"""::: ) ")" )))) "holds" (Bool (Set (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "Perm2")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p2")) ")" ))))))))) ; theorem :: MATRIX11:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) "st" (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")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "perm")))))))) ; theorem :: MATRIX11:45 (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 (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) "," (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2)) "," (Set (Var "K")) (Bool "for" (Set (Var "perm2")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "Perm2")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) "st" (Bool (Bool (Set (Var "perm2")) ($#r1_hidden :::"="::: ) (Set (Var "Perm2")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "Perm2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix11 :::"sgn"::: ) "(" (Set (Var "perm2")) "," (Set (Var "K")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M")) ")" )))))))) ; theorem :: MATRIX11:46 (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")) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "Perm")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "perm")) ($#r1_hidden :::"="::: ) (Set (Var "Perm")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "M")) ($#k4_matrix11 :::"*"::: ) (Set (Var "Perm")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M")) ")" ) "," (Set (Var "perm")) ")" ))))))) ; theorem :: MATRIX11:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "PERM")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "perm")) "is" ($#v5_matrix_2 :::"odd"::: ) ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "PERM")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "perm")))) ")" )) "holds" (Bool (Set (Set (Var "PERM")) ($#k7_relat_1 :::".:"::: ) "{" (Set (Var "p")) where p "is" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) : (Bool (Set (Var "p")) "is" ($#v5_matrix_2 :::"even"::: ) ) "}" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) : (Bool (Set (Var "q")) "is" ($#v5_matrix_2 :::"odd"::: ) ) "}" )))) ; theorem :: MATRIX11:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "ODD")) "," (Set (Var "EVEN")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "EVEN")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) : (Bool (Set (Var "p")) "is" ($#v5_matrix_2 :::"even"::: ) ) "}" ) & (Bool (Set (Var "ODD")) ($#r1_hidden :::"="::: ) "{" (Set (Var "q")) where q "is" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) : (Bool (Set (Var "q")) "is" ($#v5_matrix_2 :::"odd"::: ) ) "}" ) & (Bool (Set (Set (Var "EVEN")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "ODD"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "EVEN")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "ODD"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "EVEN"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "ODD")))) ")" ))) ; theorem :: MATRIX11:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "tr")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k1_partfun1 :::"*"::: ) (Set (Var "tr")))) & (Bool (Set (Var "tr")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) & (Bool (Set (Set (Var "tr")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "M")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )))))))) ; theorem :: MATRIX11:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "j")) ")" ))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: MATRIX11:51 (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_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "j")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: MATRIX11:52 (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")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))))) ; theorem :: MATRIX11:53 (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")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Set (Var "j")) ")" ")" ) ")" ) ")" ) ")" ")" )))))))) ; theorem :: MATRIX11:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")))))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"addFinS"::: "K" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ")" ) means :: MATRIX11:def 5 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2"))))); end; :: deftheorem defines :::"addFinS"::: MATRIX11:def 5 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k3_finseq_2 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_matrix11 :::"addFinS"::: ) (Set (Var "K")))) "iff" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2"))))) ")" ))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k5_matrix11 :::"addFinS"::: ) "K") -> ($#v1_binop_1 :::"commutative"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k5_matrix11 :::"addFinS"::: ) "K") -> ($#v2_binop_1 :::"associative"::: ) ; end; theorem :: MATRIX11:55 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "A")) ")" )))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")))) & (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_matrix11 :::"addFinS"::: ) (Set (Var "K")) ")" ) ($#k1_finsop_1 :::""**""::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ))))) ; theorem :: MATRIX11:56 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "C")) "," (Set (Var "i")) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::""**""::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k3_matrix11 :::"RLine"::: ) "(" (Set (Var "C")) "," (Set (Var "i")) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "B")) "," (Set (Var "j")) ")" ")" ) ")" ")" ) ")" ))) ")" ) ")" )))))) ; theorem :: MATRIX11:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "BIJECT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "BIJECT")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "BIJECT")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F")))) ")" ) ")" ))))) ; theorem :: MATRIX11:58 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ")" ")" ) "," (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "SF")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ")" ")" )) "st" (Bool (Bool (Set (Var "SF")) ($#r1_hidden :::"="::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) : (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "H"))) "}" )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "SF")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ")" ")" ) ")" ) "," (Set (Var "g")) ")" ))))))))) ; theorem :: MATRIX11:59 (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 "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k1_xboole_0 :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "D")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_finseq_2 :::"idseq"::: ) (Set (Var "n")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "F")) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i"))))) "implies" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))))) "implies" (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ")" ) ")" ) ")" ))))))) ; theorem :: MATRIX11:60 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool "(" (Bool "(" "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "Path")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "Path"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "Fj")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "Fj")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set (Var "Path")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "j")) "," (Set (Var "Fj")) ")" )) ")" ) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "Path")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "B")) ($#k4_matrix11 :::"*"::: ) (Set (Var "F")) ")" ) ")" ))) ")" )) ")" ) & (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ")" ) ")" ) "," (Set (Var "P")) ")" )) ")" ))))) ; theorem :: MATRIX11:61 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool "(" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k15_matrix_2 :::"FinOmega"::: ) (Set "(" ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "P")) ")" )) & (Bool "(" "for" (Set (Var "perm")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "perm"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "perm")) "," (Set (Var "A")) ")" ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k14_matrix_2 :::"-"::: ) "(" (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "B")) ")" ) "," (Set (Var "perm")) ")" ")" ))) ")" ) ")" ))))) ; theorem :: MATRIX11:62 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_6 :::"*"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "B")) ")" )))))) ;