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	mulgnn0cl	⊢ ( ( 𝑌 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 )
17	15 10 11 16	syl3anc	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 )
18		fveq1	⊢ ( 𝑥 = ( 𝑁 ∙ 𝑋 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
19		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) )
20		fvex	⊢ ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) ∈ V
21	18 19 20	fvmpt	⊢ ( ( 𝑁 ∙ 𝑋 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
22	17 21	syl	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ ( 𝑁 ∙ 𝑋 ) ) = ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) )
23		fveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
24		fvex	⊢ ( 𝑋 ‘ 𝐴 ) ∈ V
25	23 19 24	fvmpt	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
26	11 25	syl	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) = ( 𝑋 ‘ 𝐴 ) )
27	26	oveq2d	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑁 · ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝐴 ) ) ‘ 𝑋 ) ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )
28	13 22 27	3eqtr3d	⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼 ) ) → ( ( 𝑁 ∙ 𝑋 ) ‘ 𝐴 ) = ( 𝑁 · ( 𝑋 ‘ 𝐴 ) ) )