Metamath Proof Explorer

Theorem rngodir

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 
|- G = ( 1st ` R )
ringi.2 
|- H = ( 2nd ` R )
ringi.3 
|- X = ran G
Assertion rngodir 
|- ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) )

Proof

Step Hyp Ref Expression
1 ringi.1 
 |-  G = ( 1st ` R )
2 ringi.2 
 |-  H = ( 2nd ` R )
3 ringi.3 
 |-  X = ran G
4 1 2 3 rngoi 
 |-  ( R e. RingOps -> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
5 4 simprd 
 |-  ( R e. RingOps -> ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) )
6 5 simpld 
 |-  ( R e. RingOps -> A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) )
7 simp3 
 |-  ( ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
8 7 ralimi 
 |-  ( A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) -> A. z e. X ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
9 8 2ralimi 
 |-  ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) -> A. x e. X A. y e. X A. z e. X ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
10 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
11 10 oveq1d 
 |-  ( x = A -> ( ( x G y ) H z ) = ( ( A G y ) H z ) )
12 oveq1 
 |-  ( x = A -> ( x H z ) = ( A H z ) )
13 12 oveq1d 
 |-  ( x = A -> ( ( x H z ) G ( y H z ) ) = ( ( A H z ) G ( y H z ) ) )
14 11 13 eqeq12d 
 |-  ( x = A -> ( ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) <-> ( ( A G y ) H z ) = ( ( A H z ) G ( y H z ) ) ) )
15 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
16 15 oveq1d 
 |-  ( y = B -> ( ( A G y ) H z ) = ( ( A G B ) H z ) )
17 oveq1 
 |-  ( y = B -> ( y H z ) = ( B H z ) )
18 17 oveq2d 
 |-  ( y = B -> ( ( A H z ) G ( y H z ) ) = ( ( A H z ) G ( B H z ) ) )
19 16 18 eqeq12d 
 |-  ( y = B -> ( ( ( A G y ) H z ) = ( ( A H z ) G ( y H z ) ) <-> ( ( A G B ) H z ) = ( ( A H z ) G ( B H z ) ) ) )
20 oveq2 
 |-  ( z = C -> ( ( A G B ) H z ) = ( ( A G B ) H C ) )
21 oveq2 
 |-  ( z = C -> ( A H z ) = ( A H C ) )
22 oveq2 
 |-  ( z = C -> ( B H z ) = ( B H C ) )
23 21 22 oveq12d 
 |-  ( z = C -> ( ( A H z ) G ( B H z ) ) = ( ( A H C ) G ( B H C ) ) )
24 20 23 eqeq12d 
 |-  ( z = C -> ( ( ( A G B ) H z ) = ( ( A H z ) G ( B H z ) ) <-> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) ) )
25 14 19 24 rspc3v 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( A. x e. X A. y e. X A. z e. X ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) -> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) ) )
26 9 25 syl5 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) -> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) ) )
27 6 26 mpan9 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) H C ) = ( ( A H C ) G ( B H C ) ) )