This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem srgdilem

Description: Lemma for srgdi and srgdir . (Contributed by NM, 26-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgdilem.b 
|- B = ( Base ` R )
srgdilem.p 
|- .+ = ( +g ` R )
srgdilem.t 
|- .x. = ( .r ` R )
Assertion srgdilem 
|- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ 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 srgdilem.b 
 |-  B = ( Base ` R )
2 srgdilem.p 
 |-  .+ = ( +g ` R )
3 srgdilem.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 1 4 2 3 5 issrg 
 |-  ( R e. SRing <-> ( R e. CMnd /\ ( mulGrp ` R ) e. Mnd /\ 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 ) ) ) /\ ( ( ( 0g ` R ) .x. x ) = ( 0g ` R ) /\ ( x .x. ( 0g ` R ) ) = ( 0g ` R ) ) ) ) )
7 6 simp3bi 
 |-  ( R e. SRing -> 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 ) ) ) /\ ( ( ( 0g ` R ) .x. x ) = ( 0g ` R ) /\ ( x .x. ( 0g ` R ) ) = ( 0g ` R ) ) ) )
8 7 r19.21bi 
 |-  ( ( R e. SRing /\ 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 ) ) ) /\ ( ( ( 0g ` R ) .x. x ) = ( 0g ` R ) /\ ( x .x. ( 0g ` R ) ) = ( 0g ` R ) ) ) )
9 8 simpld 
 |-  ( ( R e. SRing /\ 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 ) ) ) )
10 9 3ad2antr1 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z 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 ) ) ) )
11 simpr2 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z e. B ) ) -> y e. B )
12 rsp 
 |-  ( 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 ) ) ) -> ( 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 ) ) ) ) )
13 10 11 12 sylc 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z 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 ) ) ) )
14 simpr3 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z e. B ) ) -> z e. B )
15 rsp 
 |-  ( A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) -> ( z e. B -> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
16 13 14 15 sylc 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) )
17 16 simpld 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
18 17 caovdig 
 |-  ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) )
19 16 simprd 
 |-  ( ( R e. SRing /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
20 19 caovdirg 
 |-  ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
21 18 20 jca 
 |-  ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )