:: RING_1 semantic presentation begin theorem :: RING_1:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: RING_1:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ))))) ; theorem :: RING_1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "c")))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "K")); attr "S" is :::"quasi-prime"::: means :: RING_1:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "K" "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "S") "or" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "S") "or" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "S") ")" )); end; :: deftheorem defines :::"quasi-prime"::: RING_1:def 1 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_ring_1 :::"quasi-prime"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "or" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "or" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" )) ")" ))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "K")); attr "S" is :::"prime"::: means :: RING_1:def 2 (Bool "(" (Bool "S" "is" ($#v1_subset_1 :::"proper"::: ) ) & (Bool "S" "is" ($#v1_ring_1 :::"quasi-prime"::: ) ) ")" ); end; :: deftheorem defines :::"prime"::: RING_1:def 2 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_ring_1 :::"prime"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_subset_1 :::"proper"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_ring_1 :::"quasi-prime"::: ) ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "I" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "I" is :::"quasi-maximal"::: means :: RING_1:def 3 (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" "R" "holds" (Bool "(" "not" (Bool "I" ($#r1_tarski :::"c="::: ) (Set (Var "J"))) "or" (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) "I") "or" "not" (Bool (Set (Var "J")) "is" ($#v1_subset_1 :::"proper"::: ) ) ")" )); end; :: deftheorem defines :::"quasi-maximal"::: RING_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v3_ring_1 :::"quasi-maximal"::: ) ) "iff" (Bool "for" (Set (Var "J")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool "(" "not" (Bool (Set (Var "I")) ($#r1_tarski :::"c="::: ) (Set (Var "J"))) "or" (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Set (Var "I"))) "or" "not" (Bool (Set (Var "J")) "is" ($#v1_subset_1 :::"proper"::: ) ) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "I" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "I" is :::"maximal"::: means :: RING_1:def 4 (Bool "(" (Bool "I" "is" ($#v1_subset_1 :::"proper"::: ) ) & (Bool "I" "is" ($#v3_ring_1 :::"quasi-maximal"::: ) ) ")" ); end; :: deftheorem defines :::"maximal"::: RING_1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v4_ring_1 :::"maximal"::: ) ) "iff" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_subset_1 :::"proper"::: ) ) & (Bool (Set (Var "I")) "is" ($#v3_ring_1 :::"quasi-maximal"::: ) ) ")" ) ")" ))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#v2_ring_1 :::"prime"::: ) -> ($#v1_subset_1 :::"proper"::: ) ($#v1_ring_1 :::"quasi-prime"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"))); cluster ($#v1_subset_1 :::"proper"::: ) ($#v1_ring_1 :::"quasi-prime"::: ) -> ($#v2_ring_1 :::"prime"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"))); end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#v4_ring_1 :::"maximal"::: ) -> ($#v1_subset_1 :::"proper"::: ) ($#v3_ring_1 :::"quasi-maximal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"))); cluster ($#v1_subset_1 :::"proper"::: ) ($#v3_ring_1 :::"quasi-maximal"::: ) -> ($#v4_ring_1 :::"maximal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"))); end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "R") -> ($#v1_ideal_1 :::"add-closed"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "R") -> ($#v2_ideal_1 :::"left-ideal"::: ) ($#v3_ideal_1 :::"right-ideal"::: ) ; end; theorem :: RING_1:4 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"domRing":::) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v2_ring_1 :::"prime"::: ) )) ; begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); func :::"EqRel"::: "(" "R" "," "I" ")" -> ($#m1_subset_1 :::"Relation":::) "of" "R" means :: RING_1:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) "I") ")" )); end; :: deftheorem defines :::"EqRel"::: RING_1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )) ")" )))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; theorem :: RING_1:5 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )))) ; theorem :: RING_1:6 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )))) ; theorem :: RING_1:7 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")) ")" ) ")" ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: RING_1:8 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#k1_tarski :::"}"::: ) ))) ; theorem :: RING_1:9 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: RING_1:10 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ")" )))) ; begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); func :::"QuotientRing"::: "(" "R" "," "I" ")" -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) means :: RING_1:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) "R" ")" ) ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "R" ")" ) ")" )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" "R" "," "I" ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"QuotientRing"::: RING_1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ))) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b3"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b3"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ")" ) ")" ) ")" )))); notationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); synonym "R" :::"/"::: "I" for :::"QuotientRing"::: "(" "R" "," "I" ")" ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" "R" "," "I" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; theorem :: RING_1:11 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I")) ")" ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" )))))) ; theorem :: RING_1:12 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" ) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I")) ")" ))))) ; theorem :: RING_1:13 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" )))))) ; theorem :: RING_1:14 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" )))))) ; theorem :: RING_1:15 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_ring_1 :::"EqRel"::: ) "(" (Set (Var "R")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set "(" (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I")) ")" ))))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" "R" "," "I" ")" ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "R" be ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" "R" "," "I" ")" ) -> ($#v36_algstr_0 :::"strict"::: ) ($#v5_group_1 :::"commutative"::: ) ; end; theorem :: RING_1:16 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_subset_1 :::"proper"::: ) ) "iff" (Bool (Bool "not" (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#v6_struct_0 :::"degenerated"::: ) )) ")" ))) ; theorem :: RING_1:17 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_ring_1 :::"quasi-prime"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#v1_vectsp_2 :::"domRing-like"::: ) ) ")" ))) ; theorem :: RING_1:18 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_ring_1 :::"prime"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#l6_algstr_0 :::"domRing":::)) ")" ))) ; theorem :: RING_1:19 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v5_group_1 :::"commutative"::: ) ) & (Bool (Set (Var "I")) "is" ($#v3_ring_1 :::"quasi-maximal"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ))) ; theorem :: RING_1:20 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) )) "holds" (Bool (Set (Var "I")) "is" ($#v3_ring_1 :::"quasi-maximal"::: ) ))) ; theorem :: RING_1:21 (Bool "for" (Set (Var "R")) "being" ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v4_ring_1 :::"maximal"::: ) ) "iff" (Bool (Set (Set (Var "R")) ($#k2_ring_1 :::"/"::: ) (Set (Var "I"))) "is" ($#l6_algstr_0 :::"Skew-Field":::)) ")" ))) ; registrationlet "R" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#v4_ring_1 :::"maximal"::: ) -> ($#v2_ring_1 :::"prime"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"))); end; registrationlet "R" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"Ring":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#v4_ring_1 :::"maximal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"))); end; registrationlet "R" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#v4_ring_1 :::"maximal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"))); end; registrationlet "R" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); let "I" be ($#v1_ring_1 :::"quasi-prime"::: ) ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" "R" "," "I" ")" ) -> ($#v36_algstr_0 :::"strict"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ; end; registrationlet "R" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); let "I" be ($#v3_ring_1 :::"quasi-maximal"::: ) ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "R")); cluster (Set ($#k2_ring_1 :::"QuotientRing"::: ) "(" "R" "," "I" ")" ) -> ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ; end;