Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isrng Structured version   Visualization version   GIF version

Theorem isrng 46637
Description: The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.)
Hypotheses
Ref Expression
isrng.b ๐ต = (Baseโ€˜๐‘…)
isrng.g ๐บ = (mulGrpโ€˜๐‘…)
isrng.p + = (+gโ€˜๐‘…)
isrng.t ยท = (.rโ€˜๐‘…)
Assertion
Ref Expression
isrng (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง ๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
Distinct variable groups:   ๐‘ฅ,๐ต,๐‘ฆ,๐‘ง   ๐‘ฅ,๐‘…,๐‘ฆ,๐‘ง   ๐‘ฅ, ยท ,๐‘ฆ,๐‘ง   ๐‘ฅ, + ,๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐บ(๐‘ฅ,๐‘ฆ,๐‘ง)

Proof of Theorem isrng
Dummy variables ๐‘ ๐‘Ÿ ๐‘ก ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6889 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = (mulGrpโ€˜๐‘…))
2 isrng.g . . . . . 6 ๐บ = (mulGrpโ€˜๐‘…)
31, 2eqtr4di 2791 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (mulGrpโ€˜๐‘Ÿ) = ๐บ)
43eleq1d 2819 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Smgrp โ†” ๐บ โˆˆ Smgrp))
5 fvexd 6904 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) โˆˆ V)
6 fveq2 6889 . . . . . 6 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = (Baseโ€˜๐‘…))
7 isrng.b . . . . . 6 ๐ต = (Baseโ€˜๐‘…)
86, 7eqtr4di 2791 . . . . 5 (๐‘Ÿ = ๐‘… โ†’ (Baseโ€˜๐‘Ÿ) = ๐ต)
9 fvexd 6904 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) โˆˆ V)
10 fveq2 6889 . . . . . . . 8 (๐‘Ÿ = ๐‘… โ†’ (+gโ€˜๐‘Ÿ) = (+gโ€˜๐‘…))
1110adantr 482 . . . . . . 7 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = (+gโ€˜๐‘…))
12 isrng.p . . . . . . 7 + = (+gโ€˜๐‘…)
1311, 12eqtr4di 2791 . . . . . 6 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (+gโ€˜๐‘Ÿ) = + )
14 fvexd 6904 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) โˆˆ V)
15 fveq2 6889 . . . . . . . . . 10 (๐‘Ÿ = ๐‘… โ†’ (.rโ€˜๐‘Ÿ) = (.rโ€˜๐‘…))
1615adantr 482 . . . . . . . . 9 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ (.rโ€˜๐‘Ÿ) = (.rโ€˜๐‘…))
1716adantr 482 . . . . . . . 8 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = (.rโ€˜๐‘…))
18 isrng.t . . . . . . . 8 ยท = (.rโ€˜๐‘…)
1917, 18eqtr4di 2791 . . . . . . 7 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ (.rโ€˜๐‘Ÿ) = ยท )
20 simpllr 775 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = ๐ต)
21 simpr 486 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ก = ยท )
22 eqidd 2734 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ฅ = ๐‘ฅ)
23 oveq 7412 . . . . . . . . . . . . . 14 (๐‘ = + โ†’ (๐‘ฆ๐‘๐‘ง) = (๐‘ฆ + ๐‘ง))
2423ad2antlr 726 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘๐‘ง) = (๐‘ฆ + ๐‘ง))
2521, 22, 24oveq123d 7427 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)))
26 simpr 486 . . . . . . . . . . . . . 14 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ๐‘ = + )
2726adantr 482 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ = + )
28 oveq 7412 . . . . . . . . . . . . . 14 (๐‘ก = ยท โ†’ (๐‘ฅ๐‘ก๐‘ฆ) = (๐‘ฅ ยท ๐‘ฆ))
2928adantl 483 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ฆ) = (๐‘ฅ ยท ๐‘ฆ))
30 oveq 7412 . . . . . . . . . . . . . 14 (๐‘ก = ยท โ†’ (๐‘ฅ๐‘ก๐‘ง) = (๐‘ฅ ยท ๐‘ง))
3130adantl 483 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘ก๐‘ง) = (๐‘ฅ ยท ๐‘ง))
3227, 29, 31oveq123d 7427 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)))
3325, 32eqeq12d 2749 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โ†” (๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง))))
34 oveq 7412 . . . . . . . . . . . . . 14 (๐‘ = + โ†’ (๐‘ฅ๐‘๐‘ฆ) = (๐‘ฅ + ๐‘ฆ))
3534ad2antlr 726 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฅ๐‘๐‘ฆ) = (๐‘ฅ + ๐‘ฆ))
36 eqidd 2734 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ๐‘ง = ๐‘ง)
3721, 35, 36oveq123d 7427 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง))
38 oveq 7412 . . . . . . . . . . . . . 14 (๐‘ก = ยท โ†’ (๐‘ฆ๐‘ก๐‘ง) = (๐‘ฆ ยท ๐‘ง))
3938adantl 483 . . . . . . . . . . . . 13 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (๐‘ฆ๐‘ก๐‘ง) = (๐‘ฆ ยท ๐‘ง))
4027, 31, 39oveq123d 7427 . . . . . . . . . . . 12 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))
4137, 40eqeq12d 2749 . . . . . . . . . . 11 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)) โ†” ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))
4233, 41anbi12d 632 . . . . . . . . . 10 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
4320, 42raleqbidv 3343 . . . . . . . . 9 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
4420, 43raleqbidv 3343 . . . . . . . 8 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
4520, 44raleqbidv 3343 . . . . . . 7 ((((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โˆง ๐‘ก = ยท ) โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
4614, 19, 45sbcied2 3824 . . . . . 6 (((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โˆง ๐‘ = + ) โ†’ ([(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
479, 13, 46sbcied2 3824 . . . . 5 ((๐‘Ÿ = ๐‘… โˆง ๐‘ = ๐ต) โ†’ ([(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
485, 8, 47sbcied2 3824 . . . 4 (๐‘Ÿ = ๐‘… โ†’ ([(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))) โ†” โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
494, 48anbi12d 632 . . 3 (๐‘Ÿ = ๐‘… โ†’ (((mulGrpโ€˜๐‘Ÿ) โˆˆ Smgrp โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง)))) โ†” (๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
50 df-rng 46636 . . 3 Rng = {๐‘Ÿ โˆˆ Abel โˆฃ ((mulGrpโ€˜๐‘Ÿ) โˆˆ Smgrp โˆง [(Baseโ€˜๐‘Ÿ) / ๐‘][(+gโ€˜๐‘Ÿ) / ๐‘][(.rโ€˜๐‘Ÿ) / ๐‘ก]โˆ€๐‘ฅ โˆˆ ๐‘ โˆ€๐‘ฆ โˆˆ ๐‘ โˆ€๐‘ง โˆˆ ๐‘ ((๐‘ฅ๐‘ก(๐‘ฆ๐‘๐‘ง)) = ((๐‘ฅ๐‘ก๐‘ฆ)๐‘(๐‘ฅ๐‘ก๐‘ง)) โˆง ((๐‘ฅ๐‘๐‘ฆ)๐‘ก๐‘ง) = ((๐‘ฅ๐‘ก๐‘ง)๐‘(๐‘ฆ๐‘ก๐‘ง))))}
5149, 50elrab2 3686 . 2 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง (๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
52 3anass 1096 . 2 ((๐‘… โˆˆ Abel โˆง ๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))) โ†” (๐‘… โˆˆ Abel โˆง (๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง))))))
5351, 52bitr4i 278 1 (๐‘… โˆˆ Rng โ†” (๐‘… โˆˆ Abel โˆง ๐บ โˆˆ Smgrp โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ ยท (๐‘ฆ + ๐‘ง)) = ((๐‘ฅ ยท ๐‘ฆ) + (๐‘ฅ ยท ๐‘ง)) โˆง ((๐‘ฅ + ๐‘ฆ) ยท ๐‘ง) = ((๐‘ฅ ยท ๐‘ง) + (๐‘ฆ ยท ๐‘ง)))))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3062  Vcvv 3475  [wsbc 3777  โ€˜cfv 6541  (class class class)co 7406  Basecbs 17141  +gcplusg 17194  .rcmulr 17195  Smgrpcsgrp 18606  Abelcabl 19644  mulGrpcmgp 19982  Rngcrng 46635
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 2704  ax-nul 5306
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 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-rng 46636
This theorem is referenced by:  rngabl  46638  rngmgp  46639  ringrng  46642  isringrng  46644  rngdi  46646  rngdir  46647  isrngd  46659  rngpropd  46660  prdsrngd  46664  rnglidlrng  46741  2zrngALT  46800  cznrng  46807
  Copyright terms: Public domain W3C validator