Metamath Proof Explorer

Theorem isrngd

Description: Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypotheses isrngd.b 
|- ( ph -> B = ( Base ` R ) )
isrngd.p 
|- ( ph -> .+ = ( +g ` R ) )
isrngd.t 
|- ( ph -> .x. = ( .r ` R ) )
isrngd.g 
|- ( ph -> R e. Abel )
isrngd.c 
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )
isrngd.a 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
isrngd.d 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
isrngd.e 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
Assertion isrngd 
|- ( ph -> R e. Rng )

Proof

Step Hyp Ref Expression
1 isrngd.b 
 |-  ( ph -> B = ( Base ` R ) )
2 isrngd.p 
 |-  ( ph -> .+ = ( +g ` R ) )
3 isrngd.t 
 |-  ( ph -> .x. = ( .r ` R ) )
4 isrngd.g 
 |-  ( ph -> R e. Abel )
5 isrngd.c 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )
6 isrngd.a 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
7 isrngd.d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
8 isrngd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
9 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 9 10 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
12 1 11 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` R ) ) )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 9 13 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
15 3 14 eqtrdi 
 |-  ( ph -> .x. = ( +g ` ( mulGrp ` R ) ) )
16 fvexd 
 |-  ( ph -> ( mulGrp ` R ) e. _V )
17 12 15 5 6 16 issgrpd 
 |-  ( ph -> ( mulGrp ` R ) e. Smgrp )
18 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` R ) ) )
19 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` R ) ) )
20 1 eleq2d 
 |-  ( ph -> ( z e. B <-> z e. ( Base ` R ) ) )
21 18 19 20 3anbi123d 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) )
22 21 biimpar 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( x e. B /\ y e. B /\ z e. B ) )
23 3 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> .x. = ( .r ` R ) )
24 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> x = x )
25 2 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( y .+ z ) = ( y ( +g ` R ) z ) )
26 23 24 25 oveq123d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( x ( .r ` R ) ( y ( +g ` R ) z ) ) )
27 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> .+ = ( +g ` R ) )
28 3 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. y ) = ( x ( .r ` R ) y ) )
29 3 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. z ) = ( x ( .r ` R ) z ) )
30 27 28 29 oveq123d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .+ ( x .x. z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) )
31 7 26 30 3eqtr3d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) )
32 2 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .+ y ) = ( x ( +g ` R ) y ) )
33 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> z = z )
34 23 32 33 oveq123d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x ( +g ` R ) y ) ( .r ` R ) z ) )
35 3 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( y .x. z ) = ( y ( .r ` R ) z ) )
36 27 29 35 oveq123d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. z ) .+ ( y .x. z ) ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) )
37 8 34 36 3eqtr3d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) )
38 31 37 jca 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) )
39 22 38 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) )
40 39 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) )
41 eqid 
 |-  ( +g ` R ) = ( +g ` R )
42 10 9 41 13 isrng 
 |-  ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) )
43 4 17 40 42 syl3anbrc 
 |-  ( ph -> R e. Rng )