Metamath Proof Explorer

Theorem mulgass3

Description: An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses mulgass3.b 
|- B = ( Base ` R )
mulgass3.m 
|- .x. = ( .g ` R )
mulgass3.t 
|- .X. = ( .r ` R )
Assertion mulgass3 
|- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N .x. Y ) ) = ( N .x. ( X .X. Y ) ) )

Proof

Step Hyp Ref Expression
1 mulgass3.b 
 |-  B = ( Base ` R )
2 mulgass3.m 
 |-  .x. = ( .g ` R )
3 mulgass3.t 
 |-  .X. = ( .r ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 4 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
6 5 adantr 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( oppR ` R ) e. Ring )
7 simpr1 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> N e. ZZ )
8 simpr3 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> Y e. B )
9 simpr2 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> X e. B )
10 4 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
11 eqid 
 |-  ( .g ` ( oppR ` R ) ) = ( .g ` ( oppR ` R ) )
12 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
13 10 11 12 mulgass2 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( N e. ZZ /\ Y e. B /\ X e. B ) ) -> ( ( N ( .g ` ( oppR ` R ) ) Y ) ( .r ` ( oppR ` R ) ) X ) = ( N ( .g ` ( oppR ` R ) ) ( Y ( .r ` ( oppR ` R ) ) X ) ) )
14 6 7 8 9 13 syl13anc 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( N ( .g ` ( oppR ` R ) ) Y ) ( .r ` ( oppR ` R ) ) X ) = ( N ( .g ` ( oppR ` R ) ) ( Y ( .r ` ( oppR ` R ) ) X ) ) )
15 1 3 4 12 opprmul 
 |-  ( ( N ( .g ` ( oppR ` R ) ) Y ) ( .r ` ( oppR ` R ) ) X ) = ( X .X. ( N ( .g ` ( oppR ` R ) ) Y ) )
16 1 3 4 12 opprmul 
 |-  ( Y ( .r ` ( oppR ` R ) ) X ) = ( X .X. Y )
17 16 oveq2i 
 |-  ( N ( .g ` ( oppR ` R ) ) ( Y ( .r ` ( oppR ` R ) ) X ) ) = ( N ( .g ` ( oppR ` R ) ) ( X .X. Y ) )
18 14 15 17 3eqtr3g 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N ( .g ` ( oppR ` R ) ) Y ) ) = ( N ( .g ` ( oppR ` R ) ) ( X .X. Y ) ) )
19 1 a1i 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> B = ( Base ` R ) )
20 10 a1i 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> B = ( Base ` ( oppR ` R ) ) )
21 ssv 
 |-  B C_ _V
22 21 a1i 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> B C_ _V )
23 ovexd 
 |-  ( ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` R ) y ) e. _V )
24 eqid 
 |-  ( +g ` R ) = ( +g ` R )
25 4 24 oppradd 
 |-  ( +g ` R ) = ( +g ` ( oppR ` R ) )
26 25 oveqi 
 |-  ( x ( +g ` R ) y ) = ( x ( +g ` ( oppR ` R ) ) y )
27 26 a1i 
 |-  ( ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` ( oppR ` R ) ) y ) )
28 2 11 19 20 22 23 27 mulgpropd 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> .x. = ( .g ` ( oppR ` R ) ) )
29 28 oveqd 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( N .x. Y ) = ( N ( .g ` ( oppR ` R ) ) Y ) )
30 29 oveq2d 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N .x. Y ) ) = ( X .X. ( N ( .g ` ( oppR ` R ) ) Y ) ) )
31 28 oveqd 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( N .x. ( X .X. Y ) ) = ( N ( .g ` ( oppR ` R ) ) ( X .X. Y ) ) )
32 18 30 31 3eqtr4d 
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N .x. Y ) ) = ( N .x. ( X .X. Y ) ) )