Metamath Proof Explorer

Theorem pwsmulg

Description: Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses pwsmulg.y 
|- Y = ( R ^s I )
pwsmulg.b 
|- B = ( Base ` Y )
pwsmulg.s 
|- .xb = ( .g ` Y )
pwsmulg.t 
|- .x. = ( .g ` R )
Assertion pwsmulg 
|- ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) )

Proof

Step Hyp Ref Expression
1 pwsmulg.y 
 |-  Y = ( R ^s I )
2 pwsmulg.b 
 |-  B = ( Base ` Y )
3 pwsmulg.s 
 |-  .xb = ( .g ` Y )
4 pwsmulg.t 
 |-  .x. = ( .g ` R )
5 simpll 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> R e. Mnd )
6 simplr 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> I e. V )
7 simpr3 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> A e. I )
8 1 2 pwspjmhm 
 |-  ( ( R e. Mnd /\ I e. V /\ A e. I ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) )
9 5 6 7 8 syl3anc 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) )
10 simpr1 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> N e. NN0 )
11 simpr2 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> X e. B )
12 2 3 4 mhmmulg 
 |-  ( ( ( x e. B |-> ( x ` A ) ) e. ( Y MndHom R ) /\ N e. NN0 /\ X e. B ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) )
13 9 10 11 12 syl3anc 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) )
14 1 pwsmnd 
 |-  ( ( R e. Mnd /\ I e. V ) -> Y e. Mnd )
15 14 adantr 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> Y e. Mnd )
16 2 3 mulgnn0cl 
 |-  ( ( Y e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .xb X ) e. B )
17 15 10 11 16 syl3anc 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( N .xb X ) e. B )
18 fveq1 
 |-  ( x = ( N .xb X ) -> ( x ` A ) = ( ( N .xb X ) ` A ) )
19 eqid 
 |-  ( x e. B |-> ( x ` A ) ) = ( x e. B |-> ( x ` A ) )
20 fvex 
 |-  ( ( N .xb X ) ` A ) e. _V
21 18 19 20 fvmpt 
 |-  ( ( N .xb X ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) )
22 17 21 syl 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) )
23 fveq1 
 |-  ( x = X -> ( x ` A ) = ( X ` A ) )
24 fvex 
 |-  ( X ` A ) e. _V
25 23 19 24 fvmpt 
 |-  ( X e. B -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) )
26 11 25 syl 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) )
27 26 oveq2d 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) = ( N .x. ( X ` A ) ) )
28 13 22 27 3eqtr3d 
 |-  ( ( ( R e. Mnd /\ I e. V ) /\ ( N e. NN0 /\ X e. B /\ A e. I ) ) -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) )