Metamath Proof Explorer

Theorem isrng

Description: The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020)

Ref Expression
Hypotheses isrng.b 
|- B = ( Base ` R )
isrng.g 
|- G = ( mulGrp ` R )
isrng.p 
|- .+ = ( +g ` R )
isrng.t 
|- .x. = ( .r ` R )
Assertion isrng 
|- ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isrng.b 
 |-  B = ( Base ` R )
2 isrng.g 
 |-  G = ( mulGrp ` R )
3 isrng.p 
 |-  .+ = ( +g ` R )
4 isrng.t 
 |-  .x. = ( .r ` R )
5 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
6 5 2 eqtr4di 
 |-  ( r = R -> ( mulGrp ` r ) = G )
7 6 eleq1d 
 |-  ( r = R -> ( ( mulGrp ` r ) e. Smgrp <-> G e. Smgrp ) )
8 fvexd 
 |-  ( r = R -> ( Base ` r ) e. _V )
9 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
10 9 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
11 fvexd 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) e. _V )
12 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
13 12 adantr 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
14 13 3 eqtr4di 
 |-  ( ( r = R /\ b = B ) -> ( +g ` r ) = .+ )
15 fvexd 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) e. _V )
16 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
17 16 adantr 
 |-  ( ( r = R /\ b = B ) -> ( .r ` r ) = ( .r ` R ) )
18 17 adantr 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) = ( .r ` R ) )
19 18 4 eqtr4di 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( .r ` r ) = .x. )
20 simpllr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> b = B )
21 simpr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> t = .x. )
22 eqidd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> x = x )
23 oveq 
 |-  ( p = .+ -> ( y p z ) = ( y .+ z ) )
24 23 ad2antlr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( y p z ) = ( y .+ z ) )
25 21 22 24 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t ( y p z ) ) = ( x .x. ( y .+ z ) ) )
26 simpr 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> p = .+ )
27 26 adantr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> p = .+ )
28 oveq 
 |-  ( t = .x. -> ( x t y ) = ( x .x. y ) )
29 28 adantl 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t y ) = ( x .x. y ) )
30 oveq 
 |-  ( t = .x. -> ( x t z ) = ( x .x. z ) )
31 30 adantl 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x t z ) = ( x .x. z ) )
32 27 29 31 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t y ) p ( x t z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
33 25 32 eqeq12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) <-> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) )
34 oveq 
 |-  ( p = .+ -> ( x p y ) = ( x .+ y ) )
35 34 ad2antlr 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( x p y ) = ( x .+ y ) )
36 eqidd 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> z = z )
37 21 35 36 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x p y ) t z ) = ( ( x .+ y ) .x. z ) )
38 oveq 
 |-  ( t = .x. -> ( y t z ) = ( y .x. z ) )
39 38 adantl 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( y t z ) = ( y .x. z ) )
40 27 31 39 oveq123d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( x t z ) p ( y t z ) ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
41 37 40 eqeq12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) <-> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
42 33 41 anbi12d 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
43 20 42 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
44 20 43 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
45 20 44 raleqbidv 
 |-  ( ( ( ( r = R /\ b = B ) /\ p = .+ ) /\ t = .x. ) -> ( A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
46 15 19 45 sbcied2 
 |-  ( ( ( r = R /\ b = B ) /\ p = .+ ) -> ( [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
47 11 14 46 sbcied2 
 |-  ( ( r = R /\ b = B ) -> ( [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
48 8 10 47 sbcied2 
 |-  ( r = R -> ( [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
49 7 48 anbi12d 
 |-  ( r = R -> ( ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) <-> ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
50 df-rng0 
 |-  Rng = { r e. Abel | ( ( mulGrp ` r ) e. Smgrp /\ [. ( Base ` r ) / b ]. [. ( +g ` r ) / p ]. [. ( .r ` r ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
51 49 50 elrab2 
 |-  ( R e. Rng <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
52 3anass 
 |-  ( ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) <-> ( R e. Abel /\ ( G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
53 51 52 bitr4i 
 |-  ( R e. Rng <-> ( R e. Abel /\ G e. Smgrp /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )