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

Metamath Proof Explorer

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 𝑁 ) )