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 𝑠 I
pwsexpg.b B = Base Y
pwsexpg.m M = mulGrp Y
pwsexpg.t T = mulGrp R
pwsexpg.s ˙ = M
pwsexpg.g · ˙ = T
pwsexpg.r φ R Ring
pwsexpg.i φ I V
pwsexpg.n φ N 0
pwsexpg.x φ X B
pwsexpg.a φ A I
Assertion pwsexpg φ N ˙ X A = N · ˙ X A

Proof

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