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