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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsexpg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsexpg.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
pwsexpg.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
pwsexpg.s ⊢ ∙ = ( .g ‘ 𝑀 )
pwsexpg.g ⊢ · = ( .g ‘ 𝑇 )
pwsexpg.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
pwsexpg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
pwsexpg.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
pwsexpg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
pwsexpg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
Assertion pwsexpg ( 𝜑 → ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pwsexpg.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsexpg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsexpg.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
4 pwsexpg.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
5 pwsexpg.s ⊢ ∙ = ( .g ‘ 𝑀 )
6 pwsexpg.g ⊢ · = ( .g ‘ 𝑇 )
7 pwsexpg.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 pwsexpg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 pwsexpg.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 pwsexpg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 pwsexpg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
12 1 2 3 4 7 8 11 pwspjmhmmgpd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑀 MndHom 𝑇 ) )
13 3 2 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
14 13 5 6 mhmmulg ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑀 MndHom 𝑇 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) )
15 12 9 10 14 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) )
16 1 pwsring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Ring )
17 7 8 16 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ Ring )
18 3 ringmgp ⊢ ( 𝑌 ∈ Ring → 𝑀 ∈ Mnd )
19 17 18 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
20 13 5 19 9 10 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 )
21 fveq1 ⊢ ( 𝑥 = ( 𝑁 ∙ 𝑋 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
22 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) )
23 fvex ⊢ ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) ∈ V
24 21 22 23 fvmpt ⊢ ( ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
25 20 24 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
26 fveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
27 fvex ⊢ ( 𝑋 ‘ 𝐴 ) ∈ V
28 26 22 27 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
29 10 28 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )
31 15 25 30 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )