:: MODCAT_1 semantic presentation begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode :::"LeftMod_DOMAIN"::: "of" "R" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MODCAT_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" "R")); end; :: deftheorem defines :::"LeftMod_DOMAIN"::: MODCAT_1:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "b2")) "holds" (Bool (Set (Var "x")) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")))) ")" ))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "V" -> ($#l1_vectsp_1 :::"LeftMod":::) "of" "R"; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1() ($#v7_vectsp_1 :::"strict"::: ) bbbadV8_VECTSP_1("R") bbbadV9_VECTSP_1("R") bbbadV10_VECTSP_1("R") bbbadV11_VECTSP_1("R") for ($#m1_subset_1 :::"Element"::: ) "of" "V"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode :::"LModMorphism_DOMAIN"::: "of" "R" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: MODCAT_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" "R")); end; :: deftheorem defines :::"LModMorphism_DOMAIN"::: MODCAT_1:def 2 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "b2")) "holds" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")))) ")" ))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "M" be ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Const "R")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "M" -> ($#l1_mod_2 :::"LModMorphism":::) "of" "R"; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "M" be ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Const "R")); cluster ($#v2_mod_2 :::"strict"::: ) ($#v3_mod_2 :::"LModMorphism-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "M"; end; theorem :: MODCAT_1:1 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "being" ($#v2_mod_2 :::"strict"::: ) ($#l1_mod_2 :::"LModMorphism":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "R"))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); mode :::"LModMorphism_DOMAIN"::: "of" "G" "," "H" -> ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" "R" means :: MODCAT_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "H")); end; :: deftheorem defines :::"LModMorphism_DOMAIN"::: MODCAT_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b4")) "being" ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set (Var "b4")) "holds" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )))); theorem :: MODCAT_1:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "D")) "is" ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )))) ; theorem :: MODCAT_1:3 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "f")) "being" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); func :::"Morphs"::: "(" "G" "," "H" ")" -> ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" "G" "," "H" means :: MODCAT_1:def 4 (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" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "H") ")" )); end; :: deftheorem defines :::"Morphs"::: MODCAT_1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b4")) "being" ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_modcat_1 :::"Morphs"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H"))) ")" )) ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "G", "H" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "R")); let "M" be ($#m5_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Const "G")) "," (Set (Const "H")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "M" -> ($#m1_mod_2 :::"Morphism"::: ) "of" "G" "," "H"; end; definitionlet "x", "y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#l6_algstr_0 :::"Ring":::); pred :::"GO"::: "x" "," "y" "," "R" means :: MODCAT_1:def 5 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )) & (Bool "ex" (Set (Var "G")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" "R" "st" (Bool "(" (Bool "y" ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "G"))) "#)" )) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "G")))) ")" )) ")" )); end; :: deftheorem defines :::"GO"::: MODCAT_1:def 5 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool "(" (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "R"))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )) & (Bool "ex" (Set (Var "G")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "G"))) "#)" )) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "G")))) ")" )) ")" )) ")" ))); theorem :: MODCAT_1:4 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "R"))) & (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y2")) "," (Set (Var "R")))) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))))) ; theorem :: MODCAT_1:5 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "G")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where G "is" ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN"))), f "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Num 1) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Num 1) ")" ) : (Bool verum) "}" ) & (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set ($#k1_mod_2 :::"TrivialLMod"::: ) (Set (Var "R"))) "," (Set (Var "R"))) ")" )))) ; definitionlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); func :::"LModObjects"::: "(" "UN" "," "R" ")" -> ($#m1_hidden :::"set"::: ) means :: MODCAT_1:def 6 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "G")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where G "is" ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) "UN"), f "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Num 1) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Num 1) ")" ) : (Bool verum) "}" ) & (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y")) "," "R") ")" )) ")" )); end; :: deftheorem defines :::"LModObjects"::: MODCAT_1:def 6 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "G")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) where G "is" ($#m2_grcat_1 :::"Element"::: ) "of" (Set ($#k17_grcat_1 :::"GroupObjects"::: ) (Set (Var "UN"))), f "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Num 1) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Num 1) ")" ) : (Bool verum) "}" ) & (Bool ($#r1_modcat_1 :::"GO"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "R"))) ")" )) ")" )) ")" )))); theorem :: MODCAT_1:6 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k1_mod_2 :::"TrivialLMod"::: ) (Set (Var "R"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" )))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k2_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MODCAT_1:7 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "x")) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "R")))))) ; definitionlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); :: original: :::"LModObjects"::: redefine func :::"LModObjects"::: "(" "UN" "," "R" ")" -> ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); func :::"Morphs"::: "V" -> ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" "R" means :: MODCAT_1:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m2_modcat_1 :::"Element"::: ) "of" "V" "st" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )); end; :: deftheorem defines :::"Morphs"::: MODCAT_1:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m3_modcat_1 :::"LModMorphism_DOMAIN"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")))) "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 "G")) "," (Set (Var "H")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m2_modcat_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) "is" ($#v2_mod_2 :::"strict"::: ) ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G")) "," (Set (Var "H")))) ")" )) ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); let "F" be ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Const "V"))); func :::"dom'"::: "F" -> ($#m2_modcat_1 :::"Element"::: ) "of" "V" equals :: MODCAT_1:def 8 (Set ($#k2_mod_2 :::"dom"::: ) "F"); func :::"cod'"::: "F" -> ($#m2_modcat_1 :::"Element"::: ) "of" "V" equals :: MODCAT_1:def 9 (Set ($#k3_mod_2 :::"cod"::: ) "F"); end; :: deftheorem defines :::"dom'"::: MODCAT_1:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "F"))))))); :: deftheorem defines :::"cod'"::: MODCAT_1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "F"))))))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); let "G" be ($#m2_modcat_1 :::"Element"::: ) "of" (Set (Const "V")); func :::"ID"::: "G" -> ($#v2_mod_2 :::"strict"::: ) ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) "V") equals :: MODCAT_1:def 10 (Set ($#k6_mod_2 :::"ID"::: ) "G"); end; :: deftheorem defines :::"ID"::: MODCAT_1:def 10 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "G")) "being" ($#m2_modcat_1 :::"Element"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_modcat_1 :::"ID"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_mod_2 :::"ID"::: ) (Set (Var "G"))))))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); func :::"dom"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) "V" ")" ) "," "V" means :: MODCAT_1:def 11 (Bool "for" (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "f"))))); func :::"cod"::: "V" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) "V" ")" ) "," "V" means :: MODCAT_1:def 12 (Bool "for" (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) "V") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f"))))); canceled; end; :: deftheorem defines :::"dom"::: MODCAT_1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_modcat_1 :::"dom"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "f"))))) ")" )))); :: deftheorem defines :::"cod"::: MODCAT_1:def 12 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_modcat_1 :::"cod"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f"))))) ")" )))); :: deftheorem MODCAT_1:def 13 : canceled; theorem :: MODCAT_1:8 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m2_modcat_1 :::"Element"::: ) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3"))) & (Bool (Set (Var "f")) "is" ($#m1_mod_2 :::"Morphism"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2"))) ")" ))))) ; theorem :: MODCAT_1:9 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))))))) ; theorem :: MODCAT_1:10 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Const "R")); func :::"comp"::: "V" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) "V" ")" ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) "V" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) "V" ")" ) means :: MODCAT_1:def 14 (Bool "(" (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) "V") "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it)) "iff" (Bool (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) "V") "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")))) ")" ) ")" ); end; :: deftheorem defines :::"comp"::: MODCAT_1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_modcat_1 :::"comp"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3")))) "iff" (Bool (Set ($#k5_modcat_1 :::"dom'"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k6_modcat_1 :::"cod'"::: ) (Set (Var "f")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f")))) ")" ) ")" ) ")" )))); theorem :: MODCAT_1:11 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#m1_modcat_1 :::"LeftMod_DOMAIN"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k10_modcat_1 :::"comp"::: ) (Set (Var "V")) ")" ))) "iff" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f")))) ")" )))) ; definitionlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); func :::"LModCat"::: "(" "UN" "," "R" ")" -> ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: MODCAT_1:def 15 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" ) ")" ) "," (Set "(" ($#k8_modcat_1 :::"dom"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" ) ")" ) "," (Set "(" ($#k9_modcat_1 :::"cod"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" ) ")" ) "," (Set "(" ($#k10_modcat_1 :::"comp"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"LModCat"::: MODCAT_1:def 15 : (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k11_modcat_1 :::"LModCat"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) "," (Set "(" ($#k4_modcat_1 :::"Morphs"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" ) "," (Set "(" ($#k8_modcat_1 :::"dom"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" ) "," (Set "(" ($#k9_modcat_1 :::"cod"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" ) "," (Set "(" ($#k10_modcat_1 :::"comp"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" ) "#)" )))); registrationlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k11_modcat_1 :::"LModCat"::: ) "(" "UN" "," "R" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ; end; theorem :: MODCAT_1:12 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_modcat_1 :::"LModCat"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set "(" ($#k11_modcat_1 :::"LModCat"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" )))) "iff" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" )))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); cluster -> ($#v2_mod_2 :::"strict"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" "UN" "," "R" ")" ")" )); end; theorem :: MODCAT_1:13 canceled; theorem :: MODCAT_1:14 canceled; theorem :: MODCAT_1:15 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_modcat_1 :::"LModCat"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) (Bool "for" (Set (Var "f9")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "f9")))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f9")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f9")))) ")" ))))) ; theorem :: MODCAT_1:16 (Bool "for" (Set (Var "UN")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_modcat_1 :::"LModCat"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) (Bool "for" (Set (Var "f9")) "," (Set (Var "g9")) "being" ($#m4_modcat_1 :::"Element"::: ) "of" (Set ($#k4_modcat_1 :::"Morphs"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" )) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "f9"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "g9")))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "implies" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g9"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f9")))) ")" & "(" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g9"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f9"))))) "implies" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "implies" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g9")) "," (Set (Var "f9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k10_modcat_1 :::"comp"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g9")) "," (Set (Var "f9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k10_modcat_1 :::"comp"::: ) (Set "(" ($#k3_modcat_1 :::"LModObjects"::: ) "(" (Set (Var "UN")) "," (Set (Var "R")) ")" ")" ) ")" )))) "implies" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g9")) ($#k8_mod_2 :::"*"::: ) (Set (Var "f9")))) ")" & "(" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g9")))) ")" & "(" (Bool (Bool (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_2 :::"dom"::: ) (Set (Var "g9"))))) "implies" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g"))))) "implies" (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "g9")))) ")" & "(" (Bool (Bool (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_2 :::"cod"::: ) (Set (Var "g9"))))) "implies" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) ")" ")" ))))) ; registrationlet "UN" be ($#m1_hidden :::"Universe":::); let "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k11_modcat_1 :::"LModCat"::: ) "(" "UN" "," "R" ")" ) -> ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ; end;