:: TDGROUP semantic presentation begin theorem :: TDGROUP:1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_vectsp_1 :::"G_Real"::: ) ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_vectsp_1 :::"G_Real"::: ) ) "st" (Bool (Set (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: TDGROUP:2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_vectsp_1 :::"G_Real"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_vectsp_1 :::"G_Real"::: ) )))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_vectsp_1 :::"G_Real"::: ) )))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "IT" is :::"Two_Divisible"::: means :: TDGROUP:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"Two_Divisible"::: TDGROUP:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tdgroup :::"Two_Divisible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ")" )); registration cluster (Set ($#k1_vectsp_1 :::"G_Real"::: ) ) -> ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionmode Two_Divisible_Group is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionmode Uniquely_Two_Divisible_Group is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v1_tdgroup :::"Two_Divisible"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: TDGROUP:3 (Bool "for" (Set (Var "AG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "AG")) "is" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AG")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AG")) "st" (Bool (Set (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AG")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "AG"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "AG")))) ")" ) ")" ) ")" )) ; notationlet "ADG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "ADG")); synonym "a" :::"#"::: "b" for "a" :::"+"::: "b"; end; definitionlet "ADG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"CONGRD"::: "ADG" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "ADG") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "ADG") ($#k2_zfmisc_1 :::":]"::: ) ) means :: TDGROUP:def 2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "ADG" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "c")))) ")" )); end; :: deftheorem defines :::"CONGRD"::: TDGROUP:def 2 : (Bool "for" (Set (Var "ADG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_tdgroup :::"CONGRD"::: ) (Set (Var "ADG")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "c")))) ")" )) ")" ))); definitionlet "ADG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"AV"::: "ADG" -> ($#v1_analoaf :::"strict"::: ) ($#l1_analoaf :::"AffinStruct"::: ) equals :: TDGROUP:def 3 (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "ADG") "," (Set "(" ($#k1_tdgroup :::"CONGRD"::: ) "ADG" ")" ) "#)" ); end; :: deftheorem defines :::"AV"::: TDGROUP:def 3 : (Bool "for" (Set (Var "ADG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG"))) ($#r1_hidden :::"="::: ) (Set ($#g1_analoaf :::"AffinStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG"))) "," (Set "(" ($#k1_tdgroup :::"CONGRD"::: ) (Set (Var "ADG")) ")" ) "#)" ))); registrationlet "ADG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k2_tdgroup :::"AV"::: ) "ADG") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_analoaf :::"strict"::: ) ; end; theorem :: TDGROUP:4 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "ADG")))) & (Bool (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tdgroup :::"CONGRD"::: ) (Set (Var "ADG")))) ")" )) ; definitionlet "ADG" be ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "ADG")); pred "a" "," "b" :::"==>"::: "c" "," "d" means :: TDGROUP:def 4 (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) "a" "," "b" ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) "c" "," "d" ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) "ADG" ")" ))); end; :: deftheorem defines :::"==>"::: TDGROUP:def 4 : (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_analoaf :::"CONGR"::: ) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ))) ")" ))); theorem :: TDGROUP:5 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_algstr_0 :::"#"::: ) (Set (Var "c")))) ")" ))) ; theorem :: TDGROUP:6 (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_vectsp_1 :::"G_Real"::: ) ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) ; theorem :: TDGROUP:7 (Bool "ex" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::)(Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))))) ; theorem :: TDGROUP:8 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: TDGROUP:9 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "d"))))) ; theorem :: TDGROUP:10 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "d")))))) ; theorem :: TDGROUP:11 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))) ; theorem :: TDGROUP:12 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "b")) "," (Set (Var "c")))))) ; theorem :: TDGROUP:13 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "b9")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))))) ; theorem :: TDGROUP:14 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_tdgroup :::"==>"::: ) (Set (Var "b")) "," (Set (Var "d"))))) ; theorem :: TDGROUP:15 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))))) "holds" (Bool "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG")) ")" ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" )) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) ; attr "IT" is :::"AffVect-like"::: means :: TDGROUP:def 5 (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ); end; :: deftheorem defines :::"AffVect-like"::: TDGROUP:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tdgroup :::"AffVect-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_analoaf :::"strict"::: ) ($#v2_tdgroup :::"AffVect-like"::: ) for ($#l1_analoaf :::"AffinStruct"::: ) ; end; definitionmode AffVect is ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v2_tdgroup :::"AffVect-like"::: ) ($#l1_analoaf :::"AffinStruct"::: ) ; end; theorem :: TDGROUP:16 (Bool "for" (Set (Var "AS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_analoaf :::"AffinStruct"::: ) "holds" (Bool "(" (Bool "(" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r2_analoaf :::"//"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "d")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "d"))) ")" ) ")" ) "iff" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffVect":::)) ")" )) ; theorem :: TDGROUP:17 (Bool "for" (Set (Var "ADG")) "being" ($#l2_algstr_0 :::"Uniquely_Two_Divisible_Group":::) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "ADG")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))))) "holds" (Bool (Set ($#k2_tdgroup :::"AV"::: ) (Set (Var "ADG"))) "is" ($#l1_analoaf :::"AffVect":::))) ;