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 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F ∘ S repeatS N = F ⁡ S repeatS N

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B ∧ x ∈ 0 ..^ N → S ∈ A
2 simpl2 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B ∧ x ∈ 0 ..^ N → N ∈ ℕ 0
3 simpr ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B ∧ x ∈ 0 ..^ N → x ∈ 0 ..^ N
4 repswsymb ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ x ∈ 0 ..^ N → S repeatS N ⁡ x = S
5 1 2 3 4 syl3anc ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B ∧ x ∈ 0 ..^ N → S repeatS N ⁡ x = S
6 5 fveq2d ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B ∧ x ∈ 0 ..^ N → F ⁡ S repeatS N ⁡ x = F ⁡ S
7 6 mpteq2dva ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → x ∈ 0 ..^ N ⟼ F ⁡ S repeatS N ⁡ x = x ∈ 0 ..^ N ⟼ F ⁡ S
8 simp3 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F : A ⟶ B
9 repsf ⊢ S ∈ A ∧ N ∈ ℕ 0 → S repeatS N : 0 ..^ N ⟶ A
10 9 3adant3 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → S repeatS N : 0 ..^ N ⟶ A
11 fcompt ⊢ F : A ⟶ B ∧ S repeatS N : 0 ..^ N ⟶ A → F ∘ S repeatS N = x ∈ 0 ..^ N ⟼ F ⁡ S repeatS N ⁡ x
12 8 10 11 syl2anc ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F ∘ S repeatS N = x ∈ 0 ..^ N ⟼ F ⁡ S repeatS N ⁡ x
13 fvexd ⊢ S ∈ A → F ⁡ S ∈ V
14 13 anim1i ⊢ S ∈ A ∧ N ∈ ℕ 0 → F ⁡ S ∈ V ∧ N ∈ ℕ 0
15 14 3adant3 ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F ⁡ S ∈ V ∧ N ∈ ℕ 0
16 reps ⊢ F ⁡ S ∈ V ∧ N ∈ ℕ 0 → F ⁡ S repeatS N = x ∈ 0 ..^ N ⟼ F ⁡ S
17 15 16 syl ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F ⁡ S repeatS N = x ∈ 0 ..^ N ⟼ F ⁡ S
18 7 12 17 3eqtr4d ⊢ S ∈ A ∧ N ∈ ℕ 0 ∧ F : A ⟶ B → F ∘ S repeatS N = F ⁡ S repeatS N