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

Theorem isring 20140
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 6884 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = (mulGrpโ€˜๐‘…))
2 isring.g . . . . . 6 ๐บ = (mulGrpโ€˜๐‘…)
31, 2eqtr4di 2784 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = ๐บ)
43eleq1d 2812 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โ†” ๐บ โˆˆ Mnd))
5 fvexd 6899 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) โˆˆ V)
6 fveq2 6884 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = (Baseโ€˜๐‘…))
7 isring.b . . . . . 6 ๐ต = (Baseโ€˜๐‘…)
86, 7eqtr4di 2784 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = ๐ต)
9 fvexd 6899 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) โˆˆ V)
10 simpl 482 . . . . . . . 8 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ ๐‘Ÿ = ๐‘…)
1110fveq2d 6888 . . . . . . 7 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = (+gโ€˜๐‘…))
12 isring.p . . . . . . 7 + = (+gโ€˜๐‘…)
1311, 12eqtr4di 2784 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = + )
14 fvexd 6899 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) โˆˆ V)
15 simpll 764 . . . . . . . . 9 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ๐‘Ÿ = ๐‘…)
1615fveq2d 6888 . . . . . . . 8 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = (.rโ€˜๐‘…))
17 isring.t . . . . . . . 8 ยท = (.rโ€˜๐‘…)
1816, 17eqtr4di 2784 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = ยท )
19 simpllr 773 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = ๐ต)
20 simpr 484 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ก = ยท )
21 eqidd 2727 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ฅ = ๐‘ฅ)
22 simplr 766 . . . . . . . . . . . . . 14 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = + )
2322oveqd 7421 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘๐‘ง) = (๐‘ฆ + ๐‘ง))
2420, 21, 23oveq123d 7425 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)))
2520oveqd 7421 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ฆ) = (๐‘ฅ ยท ๐‘ฆ))
2620oveqd 7421 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ง) = (๐‘ฅ ยท ๐‘ง))
2722, 25, 26oveq123d 7425 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)))
2824, 27eqeq12d 2742 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โ†” (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง))))
2922oveqd 7421 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘๐‘ฆ) = (๐‘ฅ + ๐‘ฆ))
30 eqidd 2727 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ง = ๐‘ง)
3120, 29, 30oveq123d 7425 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง))
3220oveqd 7421 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘ก๐‘ง) = (๐‘ฆ ยท ๐‘ง))
3322, 26, 32oveq123d 7425 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))
3431, 33eqeq12d 2742 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) โ†” ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))
3528, 34anbi12d 630 . . . . . . . . . 10 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3619, 35raleqbidv 3336 . . . . . . . . 9 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3719, 36raleqbidv 3336 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3819, 37raleqbidv 3336 . . . . . . 7 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
3914, 18, 38sbcied2 3819 . . . . . 6 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ([(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
409, 13, 39sbcied2 3819 . . . . 5 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ ([(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
415, 8, 40sbcied2 3819 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ([(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
424, 41anbi12d 630 . . 3 (๐‘Ÿ = ๐‘… โ†’ (((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)))) โ†” (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
43 df-ring 20138 . . 3 Ring = {๐‘Ÿ โˆˆ Grp โˆฃ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Mnd โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))))}
4442, 43elrab2 3681 . 2 (๐‘… โˆˆ Ring โ†” (๐‘… โˆˆ Grp โˆง (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
45 3anass 1092 . 2 ((๐‘… โˆˆ Grp โˆง ๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))) โ†” (๐‘… โˆˆ Grp โˆง (๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
4644, 45bitr4i 278 1 (๐‘… โˆˆ Ring โ†” (๐‘… โˆˆ Grp โˆง ๐บ โˆˆ Mnd โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3055  Vcvv 3468  [wsbc 3772  โ€˜cfv 6536  (class class class)co 7404  Basecbs 17151  +gcplusg 17204  .rcmulr 17205  Mndcmnd 18665  Grpcgrp 18861  mulGrpcmgp 20037  Ringcrg 20136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rab 3427  df-v 3470  df-sbc 3773  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-ring 20138
This theorem is referenced by:  ringgrp  20141  ringmgp  20142  ringdilem  20152  ringrng  20182  isringrng  20184  ringpropd  20185  isringd  20188  ringsrg  20194  ring1  20207  prdsringd  20218  2zrngnring  47189  cznnring  47193
  Copyright terms: Public domain W3C validator