MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isring Structured version   Visualization version   GIF version

Theorem isring 19975
Description: The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
isring.b ๐ต = (Baseโ€˜๐‘…)
isring.g ๐บ = (mulGrpโ€˜๐‘…)
isring.p + = (+gโ€˜๐‘…)
isring.t ยท = (.rโ€˜๐‘…)
Assertion
Ref Expression
isring (๐‘… โˆˆ Ring โ†” (๐‘… โˆˆ Grp โˆง ๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
Distinct variable groups:   ๐‘ฅ,๐‘ฆ,๐‘ง,๐ต   ๐‘ฅ, + ,๐‘ฆ,๐‘ง   ๐‘ฅ,๐‘…,๐‘ฆ,๐‘ง   ๐‘ฅ, ยท ,๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐บ(๐‘ฅ,๐‘ฆ,๐‘ง)

Proof of Theorem isring
Dummy variables ๐‘ ๐‘ ๐‘Ÿ ๐‘ก are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6847 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = (mulGrpโ€˜๐‘…))
2 isring.g . . . . . 6 ๐บ = (mulGrpโ€˜๐‘…)
31, 2eqtr4di 2795 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = ๐บ)
43eleq1d 2823 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โ†” ๐บ โˆˆ Mnd))
5 fvexd 6862 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) โˆˆ V)
6 fveq2 6847 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = (Baseโ€˜๐‘…))
7 isring.b . . . . . 6 ๐ต = (Baseโ€˜๐‘…)
86, 7eqtr4di 2795 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = ๐ต)
9 fvexd 6862 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) โˆˆ V)
10 simpl 484 . . . . . . . 8 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ ๐‘Ÿ = ๐‘…)
1110fveq2d 6851 . . . . . . 7 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = (+gโ€˜๐‘…))
12 isring.p . . . . . . 7 + = (+gโ€˜๐‘…)
1311, 12eqtr4di 2795 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = + )
14 fvexd 6862 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) โˆˆ V)
15 simpll 766 . . . . . . . . 9 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ๐‘Ÿ = ๐‘…)
1615fveq2d 6851 . . . . . . . 8 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = (.rโ€˜๐‘…))
17 isring.t . . . . . . . 8 ยท = (.rโ€˜๐‘…)
1816, 17eqtr4di 2795 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = ยท )
19 simpllr 775 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = ๐ต)
20 simpr 486 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ก = ยท )
21 eqidd 2738 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ฅ = ๐‘ฅ)
22 simplr 768 . . . . . . . . . . . . . 14 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = + )
2322oveqd 7379 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘๐‘ง) = (๐‘ฆ + ๐‘ง))
2420, 21, 23oveq123d 7383 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)))
2520oveqd 7379 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ฆ) = (๐‘ฅ ยท ๐‘ฆ))
2620oveqd 7379 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ง) = (๐‘ฅ ยท ๐‘ง))
2722, 25, 26oveq123d 7383 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)))
2824, 27eqeq12d 2753 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โ†” (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง))))
2922oveqd 7379 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘๐‘ฆ) = (๐‘ฅ + ๐‘ฆ))
30 eqidd 2738 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ง = ๐‘ง)
3120, 29, 30oveq123d 7383 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง))
3220oveqd 7379 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘ก๐‘ง) = (๐‘ฆ ยท ๐‘ง))
3322, 26, 32oveq123d 7383 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))
3431, 33eqeq12d 2753 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) โ†” ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))
3528, 34anbi12d 632 . . . . . . . . . 10 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3619, 35raleqbidv 3322 . . . . . . . . 9 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3719, 36raleqbidv 3322 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3819, 37raleqbidv 3322 . . . . . . 7 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3914, 18, 38sbcied2 3791 . . . . . 6 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ([(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
409, 13, 39sbcied2 3791 . . . . 5 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ ([(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
415, 8, 40sbcied2 3791 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ([(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
424, 41anbi12d 632 . . 3 (๐‘Ÿ = ๐‘… โ†’ (((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)))) โ†” (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
43 df-ring 19973 . . 3 Ring = {๐‘Ÿ โˆˆ Grp โˆฃ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))))}
4442, 43elrab2 3653 . 2 (๐‘… โˆˆ Ring โ†” (๐‘… โˆˆ Grp โˆง (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
45 3anass 1096 . 2 ((๐‘… โˆˆ Grp โˆง ๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))) โ†” (๐‘… โˆˆ Grp โˆง (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
4644, 45bitr4i 278 1 (๐‘… โˆˆ Ring โ†” (๐‘… โˆˆ Grp โˆง ๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3065  Vcvv 3448  [wsbc 3744  โ€˜cfv 6501  (class class class)co 7362  Basecbs 17090  +gcplusg 17140  .rcmulr 17141  Mndcmnd 18563  Grpcgrp 18755  mulGrpcmgp 19903  Ringcrg 19971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5268
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rab 3411  df-v 3450  df-sbc 3745  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-ring 19973
This theorem is referenced by:  ringgrp  19976  ringmgp  19977  ringdilem  19987  ringpropd  20013  isringd  20016  ringsrg  20020  ring1  20033  prdsringd  20043  ringrng  46251  isringrng  46253  2zrngnring  46324  cznnring  46328
  Copyright terms: Public domain W3C validator