:: GROUP_3 semantic presentation begin theorem :: GROUP_3:1 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: GROUP_3:2 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "G"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) ")" )) ; theorem :: GROUP_3:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" ($#v5_group_1 :::"commutative"::: ) )) ; theorem :: GROUP_3:4 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "D")))))) ; theorem :: GROUP_3:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k5_group_2 :::"*"::: ) (Set (Var "a")))) ")" )))) ; theorem :: GROUP_3:6 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H2")))) & (Bool (Set (Set (Var "H1")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "H2")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")))) ")" )))) ; theorem :: GROUP_3:7 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_3:8 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: GROUP_3:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ))))))) ; theorem :: GROUP_3:10 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: GROUP_3:11 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ))))))) ; theorem :: GROUP_3:12 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: GROUP_3:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k14_group_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_group_2 :::"*"::: ) (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k12_group_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H2")) ")" )))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); func :::"Subgroups"::: "G" -> ($#m1_hidden :::"set"::: ) means :: GROUP_3:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G") ")" )); end; :: deftheorem defines :::"Subgroups"::: GROUP_3:def 1 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) ")" )) ")" ))); registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k1_group_3 :::"Subgroups"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: GROUP_3:14 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))))) ; theorem :: GROUP_3:15 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "a" :::"|^"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: GROUP_3:def 2 (Set (Set "(" (Set "(" "b" ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) "a" ")" ) ($#k6_algstr_0 :::"*"::: ) "b"); end; :: deftheorem defines :::"|^"::: GROUP_3:def 2 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))); theorem :: GROUP_3:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "g")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: GROUP_3:17 (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 "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:18 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:19 (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 (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: GROUP_3:20 (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 (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: GROUP_3:21 (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 "(" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_group_1 :::"""::: ) )) ")" ))) ; theorem :: GROUP_3:22 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "iff" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) ")" ))) ; theorem :: GROUP_3:23 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g")) ")" ))))) ; theorem :: GROUP_3:24 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "g")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")) ")" ))))) ; theorem :: GROUP_3:25 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: GROUP_3:26 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k2_group_1 :::"""::: ) )))) ; theorem :: GROUP_3:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: GROUP_3:28 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i")) ")" ) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))))))) ; theorem :: GROUP_3:29 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: GROUP_3:30 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func "A" :::"|^"::: "B" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_3:def 3 "{" (Set "(" (Set (Var "g")) ($#k2_group_3 :::"|^"::: ) (Set (Var "h")) ")" ) where g, h "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) "B") ")" ) "}" ; end; :: deftheorem defines :::"|^"::: GROUP_3:def 3 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "g")) ($#k2_group_3 :::"|^"::: ) (Set (Var "h")) ")" ) where g, h "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) "}" ))); theorem :: GROUP_3:31 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B")))) "iff" (Bool "ex" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_3 :::"|^"::: ) (Set (Var "h")))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) ")" )))) ; theorem :: GROUP_3:32 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; theorem :: GROUP_3:33 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "B")) ($#k1_group_2 :::"""::: ) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "B")))))) ; theorem :: GROUP_3:34 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k3_group_3 :::"|^"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "C")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k3_group_3 :::"|^"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_3:35 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B")) ")" ) ($#k3_group_3 :::"|^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set "(" (Set (Var "B")) ($#k2_group_2 :::"*"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GROUP_3:36 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_group_2 :::"""::: ) ")" ) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B")) ")" ) ($#k1_group_2 :::"""::: ) )))) ; theorem :: GROUP_3:37 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_3:38 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_3:39 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_3:40 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "d")) ")" ) ($#k9_domain_1 :::"}"::: ) )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); let "g" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "A" :::"|^"::: "g" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_3:def 4 (Set "A" ($#k3_group_3 :::"|^"::: ) (Set ($#k6_domain_1 :::"{"::: ) "g" ($#k6_domain_1 :::"}"::: ) )); func "g" :::"|^"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_3:def 5 (Set (Set ($#k6_domain_1 :::"{"::: ) "g" ($#k6_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) "A"); end; :: deftheorem defines :::"|^"::: GROUP_3:def 4 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )))))); :: deftheorem defines :::"|^"::: GROUP_3:def 5 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_group_3 :::"|^"::: ) (Set (Var "A"))))))); theorem :: GROUP_3:41 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g")))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: GROUP_3:42 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_3 :::"|^"::: ) (Set (Var "h")))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ))))) ; theorem :: GROUP_3:43 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_group_2 :::"""::: ) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_3:44 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set "(" (Set (Var "B")) ($#k5_group_2 :::"*"::: ) (Set (Var "g")) ")" )))))) ; theorem :: GROUP_3:45 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g")) ")" ) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set "(" (Set (Var "g")) ($#k4_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_3:46 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A")) ")" ) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" )))))) ; theorem :: GROUP_3:47 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_3:48 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_group_3 :::"|^"::: ) (Set "(" (Set (Var "A")) ($#k5_group_2 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_3:49 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" ) ($#k5_group_3 :::"|^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_group_3 :::"|^"::: ) (Set "(" (Set (Var "b")) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" )))))) ; theorem :: GROUP_3:50 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "g")) ($#k2_group_1 :::"""::: ) ")" ) ($#k4_group_2 :::"*"::: ) (Set (Var "A")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "g"))))))) ; theorem :: GROUP_3:51 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set (Var "B")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k4_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:52 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: GROUP_3:53 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k5_group_3 :::"|^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GROUP_3:54 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set "(" (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))) ; theorem :: GROUP_3:55 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k3_group_3 :::"|^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ")" )) ; theorem :: GROUP_3:56 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ")" )) ; theorem :: GROUP_3:57 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::)) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k5_group_3 :::"|^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )))) ")" )) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func "H" :::"|^"::: "a" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_3:def 6 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" ) ($#k4_group_3 :::"|^"::: ) "a")); end; :: deftheorem defines :::"|^"::: GROUP_3:def 6 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b4")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ) ($#k4_group_3 :::"|^"::: ) (Set (Var "a")))) ")" ))))); theorem :: GROUP_3:58 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_group_3 :::"|^"::: ) (Set (Var "a")))) & (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" )) ")" ))))) ; theorem :: GROUP_3:59 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "H")) ")" ) ($#k5_group_2 :::"*"::: ) (Set (Var "a"))))))) ; theorem :: GROUP_3:60 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k6_group_3 :::"|^"::: ) (Set (Var "b"))) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" )))))) ; theorem :: GROUP_3:61 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H"))))) ; theorem :: GROUP_3:62 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k6_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) & (Bool (Set (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ")" ) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) ")" )))) ; theorem :: GROUP_3:63 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "H2")) ")" ) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" ) ($#k10_group_2 :::"/\"::: ) (Set "(" (Set (Var "H2")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:64 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k7_struct_0 :::"card"::: ) (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:65 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v8_struct_0 :::"finite"::: ) ) "iff" (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) "is" ($#v8_struct_0 :::"finite"::: ) ) ")" )))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "H" be ($#v8_struct_0 :::"finite"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "H" ($#k6_group_3 :::"|^"::: ) "a") -> ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: GROUP_3:66 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v8_struct_0 :::"finite"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:67 (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 "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" ) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:68 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))))))) ; theorem :: GROUP_3:69 (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 "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:70 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:71 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k17_group_2 :::"Index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k17_group_2 :::"Index"::: ) (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:72 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_2 :::"index"::: ) (Set "(" (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a")) ")" )))))) ; theorem :: GROUP_3:73 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_group_2 :::"="::: ) (Set (Var "H")))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); pred "a" "," "b" :::"are_conjugated"::: means :: GROUP_3:def 7 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool "a" ($#r1_hidden :::"="::: ) (Set "b" ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))))); end; :: deftheorem defines :::"are_conjugated"::: GROUP_3:def 7 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))); notationlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); antonym "a" "," "b" :::"are_not_conjugated"::: for "a" "," "b" :::"are_conjugated"::: ; end; theorem :: GROUP_3:74 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))) ; theorem :: GROUP_3:75 (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 (Var "a")) "," (Set (Var "a")) ($#r1_group_3 :::"are_conjugated"::: ) ))) ; theorem :: GROUP_3:76 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_group_3 :::"are_conjugated"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); :: original: :::"are_conjugated"::: redefine pred "a" "," "b" :::"are_conjugated"::: ; reflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")) "st" (Bool (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: GROUP_3:77 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_group_3 :::"are_conjugated"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_group_3 :::"are_conjugated"::: ) ))) ; theorem :: GROUP_3:78 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "," (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) ($#r2_group_3 :::"are_conjugated"::: ) ) "or" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) "," (Set (Var "a")) ($#r2_group_3 :::"are_conjugated"::: ) ) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))))) ; theorem :: GROUP_3:79 (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 (Var "a")) ($#k5_group_3 :::"|^"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "b")) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_group_3 :::"are_conjugated"::: ) ) "}" ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"con_class"::: "a" -> ($#m1_subset_1 :::"Subset":::) "of" "G" equals :: GROUP_3:def 8 (Set "a" ($#k5_group_3 :::"|^"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) "G" ")" ) ")" )); end; :: deftheorem defines :::"con_class"::: GROUP_3:def 8 : (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 ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_group_3 :::"|^"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" ) ")" ))))); theorem :: GROUP_3:80 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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 "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_group_3 :::"are_conjugated"::: ) ) ")" )) ")" )))) ; theorem :: GROUP_3:81 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "b")))) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_group_3 :::"are_conjugated"::: ) ) ")" ))) ; theorem :: GROUP_3:82 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))))) ; theorem :: GROUP_3:83 (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 (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))))) ; theorem :: GROUP_3:84 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))))) ; theorem :: GROUP_3:85 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "b")))) "iff" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "b")))) ")" ))) ; theorem :: GROUP_3:86 (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 "(" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "G")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GROUP_3:87 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")) ")" ) ($#k2_group_2 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")) ")" )))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); pred "A" "," "B" :::"are_conjugated"::: means :: GROUP_3:def 9 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool "A" ($#r1_hidden :::"="::: ) (Set "B" ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))))); end; :: deftheorem defines :::"are_conjugated"::: GROUP_3:def 9 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))); notationlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); antonym "A" "," "B" :::"are_not_conjugated"::: for "A" "," "B" :::"are_conjugated"::: ; end; theorem :: GROUP_3:88 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))) ; theorem :: GROUP_3:89 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "A")) "," (Set (Var "A")) ($#r3_group_3 :::"are_conjugated"::: ) ))) ; theorem :: GROUP_3:90 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "B")) "," (Set (Var "A")) ($#r3_group_3 :::"are_conjugated"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); :: original: :::"are_conjugated"::: redefine pred "A" "," "B" :::"are_conjugated"::: ; reflexivity (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")) "st" (Bool (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: GROUP_3:91 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_group_3 :::"are_conjugated"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "C")) ($#r4_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "C")) ($#r4_group_3 :::"are_conjugated"::: ) ))) ; theorem :: GROUP_3:92 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) ($#r4_group_3 :::"are_conjugated"::: ) ) "iff" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_group_3 :::"are_conjugated"::: ) ) ")" ))) ; theorem :: GROUP_3:93 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) "," (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H1"))) ($#r4_group_3 :::"are_conjugated"::: ) )) "holds" (Bool "ex" (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"con_class"::: "A" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "G" equals :: GROUP_3:def 10 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "G" : (Bool "A" "," (Set (Var "B")) ($#r4_group_3 :::"are_conjugated"::: ) ) "}" ; end; :: deftheorem defines :::"con_class"::: GROUP_3:def 10 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) : (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_group_3 :::"are_conjugated"::: ) ) "}" ))); theorem :: GROUP_3:94 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_group_3 :::"are_conjugated"::: ) ) ")" )) ")" )))) ; theorem :: GROUP_3:95 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "B")))) "iff" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_group_3 :::"are_conjugated"::: ) ) ")" ))) ; theorem :: GROUP_3:96 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))))))) ; theorem :: GROUP_3:97 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A")))))) ; theorem :: GROUP_3:98 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A")))))) ; theorem :: GROUP_3:99 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "B")))) "iff" (Bool (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "B")))) ")" ))) ; theorem :: GROUP_3:100 (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 ($#k8_group_3 :::"con_class"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) where b "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))) "}" ))) ; theorem :: GROUP_3:101 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); pred "H1" "," "H2" :::"are_conjugated"::: means :: GROUP_3:def 11 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "st" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "H1") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "H1") "#)" ) ($#r1_hidden :::"="::: ) (Set "H2" ($#k6_group_3 :::"|^"::: ) (Set (Var "g"))))); end; :: deftheorem defines :::"are_conjugated"::: GROUP_3:def 11 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r5_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "H2")) ($#k6_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))); notationlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); antonym "H1" "," "H2" :::"are_not_conjugated"::: for "H1" "," "H2" :::"are_conjugated"::: ; end; theorem :: GROUP_3:102 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r5_group_3 :::"are_conjugated"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "H2")) ($#r1_group_2 :::"="::: ) (Set (Set (Var "H1")) ($#k6_group_3 :::"|^"::: ) (Set (Var "g"))))) ")" ))) ; theorem :: GROUP_3:103 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "H1")) "," (Set (Var "H1")) ($#r5_group_3 :::"are_conjugated"::: ) ))) ; theorem :: GROUP_3:104 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r5_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "H2")) "," (Set (Var "H1")) ($#r5_group_3 :::"are_conjugated"::: ) ))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H1", "H2" be ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); :: original: :::"are_conjugated"::: redefine pred "H1" "," "H2" :::"are_conjugated"::: ; reflexivity (Bool "for" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")) "st" (Bool (Bool ((Set (Const "G")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "G")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: GROUP_3:105 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H3")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r6_group_3 :::"are_conjugated"::: ) ) & (Bool (Set (Var "H2")) "," (Set (Var "H3")) ($#r5_group_3 :::"are_conjugated"::: ) )) "holds" (Bool (Set (Var "H1")) "," (Set (Var "H3")) ($#r5_group_3 :::"are_conjugated"::: ) )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"con_class"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) "G" ")" ) means :: GROUP_3:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool "H" "," (Set (Var "H1")) ($#r5_group_3 :::"are_conjugated"::: ) ) ")" )) ")" )); end; :: deftheorem defines :::"con_class"::: GROUP_3:def 12 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_group_3 :::"Subgroups"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "H")) "," (Set (Var "H1")) ($#r5_group_3 :::"are_conjugated"::: ) ) ")" )) ")" )) ")" )))); theorem :: GROUP_3:106 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "x")) "is" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")))))) ; theorem :: GROUP_3:107 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H2")))) "iff" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r6_group_3 :::"are_conjugated"::: ) ) ")" ))) ; theorem :: GROUP_3:108 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H"))))))) ; theorem :: GROUP_3:109 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H")))))) ; theorem :: GROUP_3:110 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H2"))))) "holds" (Bool (Set (Var "H2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H1")))))) ; theorem :: GROUP_3:111 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H2")))) "iff" (Bool (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H1"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H2")))) ")" ))) ; theorem :: GROUP_3:112 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) )) "holds" (Bool (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: GROUP_3:113 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "H1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H1")) "," (Set (Var "H2")) ($#r5_group_3 :::"are_conjugated"::: ) ) "iff" (Bool (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H1"))) "," (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H2"))) ($#r4_group_3 :::"are_conjugated"::: ) ) ")" )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "IT" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); attr "IT" is :::"normal"::: means :: GROUP_3:def 13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set "IT" ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "IT") "#)" ))); end; :: deftheorem defines :::"normal"::: GROUP_3:def 13 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_group_3 :::"normal"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "IT")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "IT"))) "#)" ))) ")" ))); registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_group_3 :::"normal"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUP_3:114 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" ($#v1_group_3 :::"normal"::: ) ) & (Bool (Set ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G"))) "is" ($#v1_group_3 :::"normal"::: ) ) ")" )) ; theorem :: GROUP_3:115 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "N1")) ($#k10_group_2 :::"/\"::: ) (Set (Var "N2"))) "is" ($#v1_group_3 :::"normal"::: ) ))) ; theorem :: GROUP_3:116 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::))) "holds" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ))) ; theorem :: GROUP_3:117 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: GROUP_3:118 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: GROUP_3:119 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k14_group_2 :::"*"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))))) ")" ))) ; theorem :: GROUP_3:120 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "A")) ($#k11_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_group_2 :::"*"::: ) (Set (Var "A"))))) ")" ))) ; theorem :: GROUP_3:121 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "H")) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))))) ")" ))) ; theorem :: GROUP_3:122 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "a"))) "is" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "H")))) ")" ))) ; theorem :: GROUP_3:123 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "H")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: GROUP_3:124 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_group_2 :::"carr"::: ) (Set (Var "H"))))) ")" ))) ; theorem :: GROUP_3:125 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N2")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N1")) ")" ))))) ; theorem :: GROUP_3:126 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N1")) ")" ) ($#k2_group_2 :::"*"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "N2")) ")" )))))) ; theorem :: GROUP_3:127 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k16_group_2 :::"Right_Cosets"::: ) (Set (Var "N")))))) ; theorem :: GROUP_3:128 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k18_group_2 :::"index"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "G")); func :::"Normalizer"::: "A" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" means :: GROUP_3:def 14 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool (Set "A" ($#k4_group_3 :::"|^"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) "A") "}" ); end; :: deftheorem defines :::"Normalizer"::: GROUP_3:def 14 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_group_3 :::"Normalizer"::: ) (Set (Var "A")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "h")) where h "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) "}" ) ")" )))); theorem :: GROUP_3:129 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k10_group_3 :::"Normalizer"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "A")) ($#k4_group_3 :::"|^"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )) ")" )))) ; theorem :: GROUP_3:130 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k8_group_3 :::"con_class"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_group_2 :::"Index"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set (Var "A")) ")" ))))) ; theorem :: GROUP_3:131 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "or" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set (Var "A")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k8_group_3 :::"con_class"::: ) (Set (Var "A")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_2 :::"index"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set (Var "A")) ")" ))) ")" )))) ; theorem :: GROUP_3:132 (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 ($#k1_card_1 :::"card"::: ) (Set "(" ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_group_2 :::"Index"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))) ; theorem :: GROUP_3:133 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "or" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k7_group_3 :::"con_class"::: ) (Set (Var "a")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_2 :::"index"::: ) (Set "(" ($#k10_group_3 :::"Normalizer"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )))) ; definitionlet "G" be ($#l3_algstr_0 :::"Group":::); let "H" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); func :::"Normalizer"::: "H" -> ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" "G" equals :: GROUP_3:def 15 (Set ($#k10_group_3 :::"Normalizer"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) "H" ")" )); end; :: deftheorem defines :::"Normalizer"::: GROUP_3:def 15 : (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k10_group_3 :::"Normalizer"::: ) (Set "(" ($#k8_group_2 :::"carr"::: ) (Set (Var "H")) ")" ))))); theorem :: GROUP_3:134 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set (Set (Var "H")) ($#k6_group_3 :::"|^"::: ) (Set (Var "h"))) ($#r1_group_2 :::"="::: ) (Set (Var "H"))) ")" )) ")" )))) ; theorem :: GROUP_3:135 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k9_group_3 :::"con_class"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_group_2 :::"Index"::: ) (Set "(" ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H")) ")" ))))) ; theorem :: GROUP_3:136 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" (Bool (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "or" (Bool (Set ($#k15_group_2 :::"Left_Cosets"::: ) (Set "(" ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k9_group_3 :::"con_class"::: ) (Set (Var "H")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k18_group_2 :::"index"::: ) (Set "(" ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H")) ")" ))) ")" )))) ; theorem :: GROUP_3:137 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) "iff" (Bool (Set ($#k11_group_3 :::"Normalizer"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ))) ; theorem :: GROUP_3:138 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_group_3 :::"Normalizer"::: ) (Set "(" ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ; theorem :: GROUP_3:139 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k11_group_3 :::"Normalizer"::: ) (Set "(" ($#k7_group_2 :::"(Omega)."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "G")))) ;