Metamath Proof Explorer

Theorem pwsexpg

Description: Value of a group exponentiation in a structure power. Compare pwsmulg . (Contributed by SN, 30-Jul-2024)

Ref Expression
Hypotheses pwsexpg.y 
|- Y = ( R ^s I )
pwsexpg.b 
|- B = ( Base ` Y )
pwsexpg.m 
|- M = ( mulGrp ` Y )
pwsexpg.t 
|- T = ( mulGrp ` R )
pwsexpg.s 
|- .xb = ( .g ` M )
pwsexpg.g 
|- .x. = ( .g ` T )
pwsexpg.r 
|- ( ph -> R e. Ring )
pwsexpg.i 
|- ( ph -> I e. V )
pwsexpg.n 
|- ( ph -> N e. NN0 )
pwsexpg.x 
|- ( ph -> X e. B )
pwsexpg.a 
|- ( ph -> A e. I )
Assertion pwsexpg 
|- ( ph -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) )

Proof

Step Hyp Ref Expression
1 pwsexpg.y 
 |-  Y = ( R ^s I )
2 pwsexpg.b 
 |-  B = ( Base ` Y )
3 pwsexpg.m 
 |-  M = ( mulGrp ` Y )
4 pwsexpg.t 
 |-  T = ( mulGrp ` R )
5 pwsexpg.s 
 |-  .xb = ( .g ` M )
6 pwsexpg.g 
 |-  .x. = ( .g ` T )
7 pwsexpg.r 
 |-  ( ph -> R e. Ring )
8 pwsexpg.i 
 |-  ( ph -> I e. V )
9 pwsexpg.n 
 |-  ( ph -> N e. NN0 )
10 pwsexpg.x 
 |-  ( ph -> X e. B )
11 pwsexpg.a 
 |-  ( ph -> A e. I )
12 1 2 3 4 7 8 11 pwspjmhmmgpd 
 |-  ( ph -> ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) )
13 3 2 mgpbas 
 |-  B = ( Base ` M )
14 13 5 6 mhmmulg 
 |-  ( ( ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) /\ N e. NN0 /\ X e. B ) -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) )
15 12 9 10 14 syl3anc 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) )
16 1 pwsring 
 |-  ( ( R e. Ring /\ I e. V ) -> Y e. Ring )
17 7 8 16 syl2anc 
 |-  ( ph -> Y e. Ring )
18 3 ringmgp 
 |-  ( Y e. Ring -> M e. Mnd )
19 17 18 syl 
 |-  ( ph -> M e. Mnd )
20 13 5 mulgnn0cl 
 |-  ( ( M e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .xb X ) e. B )
21 19 9 10 20 syl3anc 
 |-  ( ph -> ( N .xb X ) e. B )
22 fveq1 
 |-  ( x = ( N .xb X ) -> ( x ` A ) = ( ( N .xb X ) ` A ) )
23 eqid 
 |-  ( x e. B |-> ( x ` A ) ) = ( x e. B |-> ( x ` A ) )
24 fvex 
 |-  ( ( N .xb X ) ` A ) e. _V
25 22 23 24 fvmpt 
 |-  ( ( N .xb X ) e. B -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) )
26 21 25 syl 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` ( N .xb X ) ) = ( ( N .xb X ) ` A ) )
27 fveq1 
 |-  ( x = X -> ( x ` A ) = ( X ` A ) )
28 fvex 
 |-  ( X ` A ) e. _V
29 27 23 28 fvmpt 
 |-  ( X e. B -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) )
30 10 29 syl 
 |-  ( ph -> ( ( x e. B |-> ( x ` A ) ) ` X ) = ( X ` A ) )
31 30 oveq2d 
 |-  ( ph -> ( N .x. ( ( x e. B |-> ( x ` A ) ) ` X ) ) = ( N .x. ( X ` A ) ) )
32 15 26 31 3eqtr3d 
 |-  ( ph -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) )