:: MATRIX_7 semantic presentation begin theorem :: MATRIX_7:1 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) )) "or" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 2) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ")" )) ; theorem :: MATRIX_7:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) )) "or" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 2) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 2) ")" ))) ; theorem :: MATRIX_7:3 (Bool (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Num 2) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) ) ($#k2_tarski :::"}"::: ) )) ; theorem :: MATRIX_7:4 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 2) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: MATRIX_7:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) & (Bool (Set (Var "k2")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Num 1) "," (Set (Var "k2")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "k2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" )))))) ; theorem :: MATRIX_7:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" ))))) ; theorem :: MATRIX_7:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ")" ))))) ; theorem :: MATRIX_7:8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Num 2) ")" ) "st" (Bool (Bool "ex" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "q")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" ))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 2) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: MATRIX_7:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "pa")) "," (Set (Var "pb")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "pa"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "pb")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "pb")) ($#k1_partfun1 :::"*"::: ) (Set (Var "pa"))))))) ; theorem :: MATRIX_7:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Num 2) ")" ) "st" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "p")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) & (Bool "ex" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "q")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" ))) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: MATRIX_7:11 (Bool "for" (Set (Var "l")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "l"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Set (Var "l")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) "is" ($#v4_matrix_2 :::"being_transposition"::: ) ) ")" )) ")" )) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Num 2) ($#k10_finseq_1 :::"*>"::: ) ))) ; theorem :: MATRIX_7:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Num 2) "," (Set (Var "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 2) ")" ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Num 2) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 2) "," (Num 1) ")" ")" ) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); :: original: :::"*"::: redefine func "a" :::"*"::: "M" -> ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; theorem :: MATRIX_7:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) ")" ))) ; theorem :: MATRIX_7:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "i")) "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 (Var "n"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))))))) ; theorem :: MATRIX_7:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k1_matrix_3 :::"0."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; definitionlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; func :::"IFIN"::: "(" "x" "," "y" "," "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: MATRIX_7:def 1 "a" if (Bool "x" ($#r2_hidden :::"in"::: ) "y") otherwise "b"; end; :: deftheorem defines :::"IFIN"::: MATRIX_7:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) "implies" (Bool (Set ($#k2_matrix_7 :::"IFIN"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))))) "implies" (Bool (Set ($#k2_matrix_7 :::"IFIN"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ")" )); theorem :: MATRIX_7:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); :: original: :::"diagonal"::: redefine attr "M" is :::"diagonal"::: means :: MATRIX_7:def 2 (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"::: ) "n")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n")) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))); end; :: deftheorem defines :::"diagonal"::: MATRIX_7: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 "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matrix_1 :::"diagonal"::: ) ) "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 (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 (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))); theorem :: MATRIX_7:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "A")) "is" bbbadV2_MATRIX_1((Set (Var "b1"))))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" ($#k13_matrix_3 :::"diagonal_of_Matrix"::: ) (Set (Var "A")) ")" )))))) ; theorem :: MATRIX_7:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "p")) ($#k2_funct_2 :::"""::: ) ) "is" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n")))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Const "n"))); :: original: :::"""::: redefine func "p" :::"""::: -> ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) "n"); end; theorem :: MATRIX_7:19 (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")) "holds" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")))))) ; theorem :: MATRIX_7:20 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "f2")) ")" ) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "f1")) ")" ) ($#k2_group_1 :::"""::: ) ")" ))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "G")); canceled; func "f" :::"""::: -> ($#m2_finseq_1 :::"FinSequence":::) "of" "G" means :: MATRIX_7:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k2_group_1 :::"""::: ) )) ")" ) ")" ); end; :: deftheorem MATRIX_7:def 3 : canceled; :: deftheorem defines :::"""::: MATRIX_7:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k4_matrix_7 :::"""::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k2_group_1 :::"""::: ) )) ")" ) ")" ) ")" ))); theorem :: MATRIX_7:21 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ")" ) ($#k4_matrix_7 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))))) ; theorem :: MATRIX_7:22 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ($#k4_matrix_7 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k4_matrix_7 :::"""::: ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "g")) ($#k4_matrix_7 :::"""::: ) ")" ))))) ; theorem :: MATRIX_7:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k4_matrix_7 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: MATRIX_7:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) ($#k4_matrix_7 :::"""::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: MATRIX_7:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set "(" (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) ($#k4_matrix_7 :::"""::: ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: MATRIX_7:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "f")) ")" ) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set "(" ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "f")) ")" ) ($#k4_matrix_7 :::"""::: ) ")" ))))) ; theorem :: MATRIX_7:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "ITP")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "ITG")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k13_matrix_2 :::"Group_of_Perm"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "ITG")) ($#r1_hidden :::"="::: ) (Set (Var "ITP"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "ITP")) ($#k3_matrix_7 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "ITG")) ($#k2_group_1 :::"""::: ) ))))) ; theorem :: MATRIX_7:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "IT")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_matrix_2 :::"even"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k3_matrix_7 :::"""::: ) ) "is" ($#v5_matrix_2 :::"even"::: ) ) ")" ))) ; theorem :: MATRIX_7:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set (Var "x")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k14_matrix_2 :::"-"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "p")) ($#k3_matrix_7 :::"""::: ) ")" ) ")" )))))) ; theorem :: MATRIX_7:30 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f1")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f2")) ")" ))))) ; theorem :: MATRIX_7:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "R1")) "," (Set (Var "R2")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "R2")))))) ; theorem :: MATRIX_7:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))))) ; theorem :: MATRIX_7:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "g")))))))) ; theorem :: MATRIX_7:34 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))) "is" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K"))))))) ; theorem :: MATRIX_7:35 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set "(" (Set (Var "p")) ($#k3_matrix_7 :::"""::: ) ")" ) "," (Set "(" (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrix_3 :::"Path_matrix"::: ) "(" (Set (Var "p")) "," (Set (Var "A")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_matrix_7 :::"""::: ) ")" ))))))) ; theorem :: MATRIX_7:36 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_matrix_2 :::"Element"::: ) "of" (Set ($#k12_matrix_2 :::"Permutations"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set "(" (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_matrix_7 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_matrix_3 :::"Path_product"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")))))))) ; theorem :: MATRIX_7:37 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ")" )))))) ;