This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsmulg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsmulg.s ⊢ ∙ = ( .g ‘ 𝑌 )
pwsmulg.t ⊢ · = ( .g ‘ 𝑅 )
Assertion pwsmulg ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pwsmulg.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsmulg.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 pwsmulg.s ⊢ ∙ = ( .g ‘ 𝑌 )
4 pwsmulg.t ⊢ · = ( .g ‘ 𝑅 )
5 simpll ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝑅 ∈ Mnd )
6 simplr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝐼 ∈ 𝑉 )
7 simpr3 ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝐴 ∈ 𝐼 )
8 1 2 pwspjmhm ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )
9 5 6 7 8 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )
10 simpr1 ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝑁 ∈ ℕ0 )
11 simpr2 ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝑋 ∈ 𝐵 )
12 2 3 4 mhmmulg ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ∈ ( 𝑌 MndHom 𝑅 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) )
13 9 10 11 12 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) )
14 1 pwsmnd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Mnd )
15 14 adantr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → 𝑌 ∈ Mnd )
16 2 3 15 10 11 mulgnn0cld ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 )
17 fveq1 ⊢ ( 𝑥 = ( 𝑁 ∙ 𝑋 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
18 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) )
19 fvex ⊢ ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) ∈ V
20 17 18 19 fvmpt ⊢ ( ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
21 16 20 syl ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
22 fveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
23 fvex ⊢ ( 𝑋 ‘ 𝐴 ) ∈ V
24 22 18 23 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
25 11 24 syl ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
26 25 oveq2d ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )
27 13 21 26 3eqtr3d ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )