:: MOD_4 semantic presentation begin registrationlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "G") -> ($#v3_funct_2 :::"bijective"::: ) ; end; definitionlet "A", "B", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "C")); :: original: :::"~"::: redefine func :::"~"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," "C"; end; theorem :: MOD_4:1 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mod_4 :::"~"::: ) (Set (Var "f")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"opp"::: "K" -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: MOD_4:def 1 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") "," (Set "(" ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) "K" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) "#)" ); end; :: deftheorem defines :::"opp"::: MOD_4:def 1 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "," (Set "(" ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) "#)" ))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: MOD_4:2 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "K"))) "#)" )) & "(" (Bool (Bool (Set (Var "K")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Var "K")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Var "K")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) )) "implies" (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K")))) ")" & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Scalar":::) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K"))) ")" ) ")" ) ")" )) ; theorem :: MOD_4:3 (Bool "(" (Bool "(" "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "c")) ")" ))) ")" )) ")" ) ")" ) ")" ) ")" ) ; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v36_algstr_0 :::"strict"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ; end; theorem :: MOD_4:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) "is" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"Ring":::))) ; theorem :: MOD_4:5 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) "is" ($#l6_algstr_0 :::"Skew-Field":::))) ; registrationlet "K" be ($#l6_algstr_0 :::"Skew-Field":::); cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: MOD_4:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) "is" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"Field":::))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster (Set ($#k2_mod_4 :::"opp"::: ) "K") -> ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ; end; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); func :::"opp"::: "V" -> ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set ($#k2_mod_4 :::"opp"::: ) "K") means :: MOD_4:def 2 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) "K" ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "st" (Bool (Bool (Set (Var "o")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" "V")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) "," (Set (Var "o")) "#)" ))); end; :: deftheorem defines :::"opp"::: MOD_4:def 2 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool (Bool (Set (Var "o")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V")))))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "o")) "#)" ))) ")" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster (Set ($#k3_mod_4 :::"opp"::: ) "V") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_vectsp_2 :::"strict"::: ) ; end; theorem :: MOD_4:7 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) ")" ) ")" ) ")" ))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "o" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); func :::"opp"::: "o" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) "V" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) "K" ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) "V" ")" )) equals :: MOD_4:def 3 (Set ($#k1_mod_4 :::"~"::: ) "o"); end; :: deftheorem defines :::"opp"::: MOD_4:def 3 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool (Set ($#k4_mod_4 :::"opp"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set (Var "o"))))))); theorem :: MOD_4:8 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) "holds" (Bool (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k4_mod_4 :::"opp"::: ) (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))))))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "K")); func :::"opp"::: "W" -> ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set ($#k2_mod_4 :::"opp"::: ) "K") means :: MOD_4:def 4 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) "K" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") "st" (Bool (Bool (Set (Var "o")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" "W")))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "W") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "W" ")" ) "," (Set (Var "o")) "#)" ))); end; :: deftheorem defines :::"opp"::: MOD_4:def 4 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "st" (Bool (Bool (Set (Var "o")) ($#r1_funct_2 :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "W")))))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "W"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) "," (Set (Var "o")) "#)" ))) ")" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "K")); cluster (Set ($#k5_mod_4 :::"opp"::: ) "W") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ; end; theorem :: MOD_4:9 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "W"))) "#)" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) ")" ) ")" ) ")" ))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "K")); let "o" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "W"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "W"))); func :::"opp"::: "o" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) "K" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) "W" ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) "W" ")" )) equals :: MOD_4:def 5 (Set ($#k1_mod_4 :::"~"::: ) "o"); end; :: deftheorem defines :::"opp"::: MOD_4:def 5 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "holds" (Bool (Set ($#k6_mod_4 :::"opp"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mod_4 :::"~"::: ) (Set (Var "o"))))))); theorem :: MOD_4:10 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) "holds" (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) ($#r8_binop_1 :::"="::: ) (Set ($#k6_mod_4 :::"opp"::: ) (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "W"))))))) ; theorem :: MOD_4:11 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set "(" ($#k4_mod_4 :::"opp"::: ) (Set (Var "o")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "v")) ")" ))))))))) ; theorem :: MOD_4:12 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "L")) ($#r1_hidden :::"="::: ) (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")))) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))))))))) ; theorem :: MOD_4:13 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Set (Var "w1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2"))))))))) ; theorem :: MOD_4:14 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set "(" ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set "(" ($#k6_mod_4 :::"opp"::: ) (Set (Var "o")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "o")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" ))))))))) ; theorem :: MOD_4:15 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))))))))) ; theorem :: MOD_4:16 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "w1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "w2")))) "holds" (Bool (Set (Set (Var "w1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2"))))))))) ; theorem :: MOD_4:17 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) "holds" (Bool (Set ($#k5_mod_4 :::"opp"::: ) (Set "(" ($#k3_mod_4 :::"opp"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" )))) ; theorem :: MOD_4:18 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "K")) "holds" (Bool (Set ($#k3_mod_4 :::"opp"::: ) (Set "(" ($#k5_mod_4 :::"opp"::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "W"))) "," (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "W"))) "#)" )))) ; theorem :: MOD_4:19 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_mod_4 :::"opp"::: ) (Set (Var "V"))) "is" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); cluster (Set ($#k3_mod_4 :::"opp"::: ) "V") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_vectsp_2 :::"strict"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ; end; theorem :: MOD_4:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k5_mod_4 :::"opp"::: ) (Set (Var "W"))) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set ($#k2_mod_4 :::"opp"::: ) (Set (Var "K")))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "W" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "K")); cluster (Set ($#k5_mod_4 :::"opp"::: ) "W") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; begin definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); attr "IT" is :::"antimultiplicative"::: means :: MOD_4:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "K" "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"antimultiplicative"::: MOD_4:def 6 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_mod_4 :::"antimultiplicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); attr "IT" is :::"antilinear"::: means :: MOD_4:def 7 (Bool "(" (Bool "IT" "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool "IT" "is" ($#v1_mod_4 :::"antimultiplicative"::: ) ) & (Bool "IT" "is" ($#v6_group_1 :::"unity-preserving"::: ) ) ")" ); end; :: deftheorem defines :::"antilinear"::: MOD_4:def 7 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_mod_4 :::"antilinear"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v1_mod_4 :::"antimultiplicative"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v6_group_1 :::"unity-preserving"::: ) ) ")" ) ")" ))); registrationlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_mod_4 :::"antilinear"::: ) -> ($#v6_group_1 :::"unity-preserving"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_4 :::"antimultiplicative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v6_group_1 :::"unity-preserving"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_4 :::"antimultiplicative"::: ) -> ($#v2_mod_4 :::"antilinear"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); attr "IT" is :::"monomorphism"::: means :: MOD_4:def 8 (Bool "(" (Bool "IT" "is" ($#v1_ringcat1 :::"linear"::: ) ) & (Bool "IT" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ); attr "IT" is :::"antimonomorphism"::: means :: MOD_4:def 9 (Bool "(" (Bool "IT" "is" ($#v2_mod_4 :::"antilinear"::: ) ) & (Bool "IT" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ); end; :: deftheorem defines :::"monomorphism"::: MOD_4:def 8 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_mod_4 :::"monomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_ringcat1 :::"linear"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ) ")" ))); :: deftheorem defines :::"antimonomorphism"::: MOD_4:def 9 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_mod_4 :::"antimonomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_mod_4 :::"antilinear"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ) ")" ))); definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); attr "IT" is :::"epimorphism"::: means :: MOD_4:def 10 (Bool "(" (Bool "IT" "is" ($#v1_ringcat1 :::"linear"::: ) ) & (Bool "IT" "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ); attr "IT" is :::"antiepimorphism"::: means :: MOD_4:def 11 (Bool "(" (Bool "IT" "is" ($#v2_mod_4 :::"antilinear"::: ) ) & (Bool "IT" "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ); end; :: deftheorem defines :::"epimorphism"::: MOD_4:def 10 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_mod_4 :::"epimorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_ringcat1 :::"linear"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))); :: deftheorem defines :::"antiepimorphism"::: MOD_4:def 11 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_mod_4 :::"antiepimorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_mod_4 :::"antilinear"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))); definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); attr "IT" is :::"isomorphism"::: means :: MOD_4:def 12 (Bool "(" (Bool "IT" "is" ($#v3_mod_4 :::"monomorphism"::: ) ) & (Bool "IT" "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ); attr "IT" is :::"antiisomorphism"::: means :: MOD_4:def 13 (Bool "(" (Bool "IT" "is" ($#v4_mod_4 :::"antimonomorphism"::: ) ) & (Bool "IT" "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ); end; :: deftheorem defines :::"isomorphism"::: MOD_4:def 12 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_mod_4 :::"monomorphism"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))); :: deftheorem defines :::"antiisomorphism"::: MOD_4:def 13 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_mod_4 :::"antimonomorphism"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "K")); attr "IT" is :::"endomorphism"::: means :: MOD_4:def 14 (Bool "IT" "is" ($#v1_ringcat1 :::"linear"::: ) ); attr "IT" is :::"antiendomorphism"::: means :: MOD_4:def 15 (Bool "IT" "is" ($#v2_mod_4 :::"antilinear"::: ) ); end; :: deftheorem defines :::"endomorphism"::: MOD_4:def 14 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_mod_4 :::"endomorphism"::: ) ) "iff" (Bool (Set (Var "IT")) "is" ($#v1_ringcat1 :::"linear"::: ) ) ")" ))); :: deftheorem defines :::"antiendomorphism"::: MOD_4:def 15 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_mod_4 :::"antiendomorphism"::: ) ) "iff" (Bool (Set (Var "IT")) "is" ($#v2_mod_4 :::"antilinear"::: ) ) ")" ))); theorem :: MOD_4:21 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "J")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) & (Bool (Set (Var "J")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "J")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))) ; theorem :: MOD_4:22 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "J")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) & (Bool (Set (Var "J")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "J")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))) ; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "K") -> ($#v7_mod_4 :::"isomorphism"::: ) ; end; theorem :: MOD_4:23 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "J")) "is" ($#v1_ringcat1 :::"linear"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )))) ; theorem :: MOD_4:24 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "J")) "is" ($#v2_mod_4 :::"antilinear"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )))) ; theorem :: MOD_4:25 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool "(" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "K"))) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool (Set (Var "K")) "is" ($#l6_algstr_0 :::"comRing":::)) ")" )) ; theorem :: MOD_4:26 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Skew-Field":::) "holds" (Bool "(" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "K"))) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool (Set (Var "K")) "is" ($#l6_algstr_0 :::"Field":::)) ")" )) ; begin definitionlet "K", "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "J" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); func :::"opp"::: "J" -> ($#m1_subset_1 :::"Function":::) "of" "K" "," (Set "(" ($#k2_mod_4 :::"opp"::: ) "L" ")" ) equals :: MOD_4:def 16 "J"; end; :: deftheorem defines :::"opp"::: MOD_4:def 16 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) ($#r1_hidden :::"="::: ) (Set (Var "J"))))); theorem :: MOD_4:27 canceled; theorem :: MOD_4:28 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v1_ringcat1 :::"linear"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v2_mod_4 :::"antilinear"::: ) ) ")" )))) ; theorem :: MOD_4:29 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v2_mod_4 :::"antilinear"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v1_ringcat1 :::"linear"::: ) ) ")" )))) ; theorem :: MOD_4:30 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v3_mod_4 :::"monomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v4_mod_4 :::"antimonomorphism"::: ) ) ")" )))) ; theorem :: MOD_4:31 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v4_mod_4 :::"antimonomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v3_mod_4 :::"monomorphism"::: ) ) ")" )))) ; theorem :: MOD_4:32 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v5_mod_4 :::"epimorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v6_mod_4 :::"antiepimorphism"::: ) ) ")" )))) ; theorem :: MOD_4:33 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v6_mod_4 :::"antiepimorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v5_mod_4 :::"epimorphism"::: ) ) ")" )))) ; theorem :: MOD_4:34 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) ")" )))) ; theorem :: MOD_4:35 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) ")" )))) ; theorem :: MOD_4:36 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v9_mod_4 :::"endomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v2_mod_4 :::"antilinear"::: ) ) ")" ))) ; theorem :: MOD_4:37 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v10_mod_4 :::"antiendomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v1_ringcat1 :::"linear"::: ) ) ")" ))) ; theorem :: MOD_4:38 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) ")" ))) ; theorem :: MOD_4:39 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "J")) "is" ($#v8_mod_4 :::"antiisomorphism"::: ) ) "iff" (Bool (Set ($#k7_mod_4 :::"opp"::: ) (Set (Var "J"))) "is" ($#v7_mod_4 :::"isomorphism"::: ) ) ")" ))) ; begin definitionlet "G", "H" be ($#l2_algstr_0 :::"AddGroup":::); mode Homomorphism of "G" "," "H" is ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Function":::) "of" "G" "," "H"; end; definitionlet "G" be ($#l2_algstr_0 :::"AddGroup":::); mode Endomorphism of "G" is ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "G"; end; registrationlet "G" be ($#l2_algstr_0 :::"AddGroup":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_funct_2 :::"bijective"::: ) ($#v13_vectsp_1 :::"additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "G" be ($#l2_algstr_0 :::"AddGroup":::); mode Automorphism of "G" is ($#v3_funct_2 :::"bijective"::: ) ($#m1_subset_1 :::"Endomorphism":::) "of" "G"; end; theorem :: MOD_4:40 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l2_algstr_0 :::"AddGroup":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "H")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )))) ; begin definitionlet "K", "L" be ($#l6_algstr_0 :::"Ring":::); let "J" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "L")); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "L")); mode :::"Homomorphism"::: "of" "J" "," "V" "," "W" -> ($#m1_subset_1 :::"Function":::) "of" "V" "," "W" means :: MOD_4:def 17 (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "K" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "J" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"Homomorphism"::: MOD_4:def 17 : (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_mod_4 :::"Homomorphism"::: ) "of" (Set (Var "J")) "," (Set (Var "V")) "," (Set (Var "W"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ) ")" ) ")" )))))); theorem :: MOD_4:41 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_grcat_1 :::"ZeroMap"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) "is" ($#m1_mod_4 :::"Homomorphism"::: ) "of" (Set (Var "J")) "," (Set (Var "V")) "," (Set (Var "W"))))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "J" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "K")) "," (Set (Const "K")); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode Endomorphism of "J" "," "V" is ($#m1_mod_4 :::"Homomorphism"::: ) "of" "J" "," "V" "," "V"; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V", "W" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode Homomorphism of "V" "," "W" is ($#m1_mod_4 :::"Homomorphism"::: ) "of" (Set ($#k3_struct_0 :::"id"::: ) "K") "," "V" "," "W"; end; theorem :: MOD_4:42 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_mod_4 :::"Homomorphism":::) "of" (Set (Var "V")) "," (Set (Var "W"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ) ")" ) ")" )))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode Endomorphism of "V" is ($#m1_mod_4 :::"Homomorphism":::) "of" "V" "," "V"; end;