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 ) ) )