Theorem repsco

Description: Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018)

	Ref	Expression
Assertion	repsco	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 repeatS 𝑁 ) ) = ( ( 𝐹 ‘ 𝑆 ) repeatS 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ 𝐴 )
2		simpl2	⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
3		simpr	⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
4		repswsymb	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) = 𝑆 )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) = 𝑆 )
6	5	fveq2d	⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑆 ) )
7	6	mpteq2dva	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ 𝑆 ) ) )
8		simp3	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
9		repsf	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝐴 )
10	9	3adant3	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝐴 )
11		fcompt	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝐴 ) → ( 𝐹 ∘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) ) ) )
12	8 10 11	syl2anc	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 repeatS 𝑁 ) ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ ( ( 𝑆 repeatS 𝑁 ) ‘ 𝑥 ) ) ) )
13		fvexd	⊢ ( 𝑆 ∈ 𝐴 → ( 𝐹 ‘ 𝑆 ) ∈ V )
14	13	anim1i	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑆 ) ∈ V ∧ 𝑁 ∈ ℕ0 ) )
15	14	3adant3	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ‘ 𝑆 ) ∈ V ∧ 𝑁 ∈ ℕ0 ) )
16		reps	⊢ ( ( ( 𝐹 ‘ 𝑆 ) ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑆 ) repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ 𝑆 ) ) )
17	15 16	syl	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ‘ 𝑆 ) repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐹 ‘ 𝑆 ) ) )
18	7 12 17	3eqtr4d	⊢ ( ( 𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 repeatS 𝑁 ) ) = ( ( 𝐹 ‘ 𝑆 ) repeatS 𝑁 ) )