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

Metamath Proof Explorer

Theorem repsw3

Description: The "repeated symbol word" of length three. (Contributed by AV, 6-Nov-2018)

Ref Expression
Assertion repsw3 ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 3 ) = ⟨“ 𝑆 𝑆 𝑆 ”⟩ )

Proof

Step Hyp Ref Expression
1 df-s3 ⊢ ⟨“ 𝑆 𝑆 𝑆 ”⟩ = ( ⟨“ 𝑆 𝑆 ”⟩ ++ ⟨“ 𝑆 ”⟩ )
2 2nn0 ⊢ 2 ∈ ℕ0
3 1nn0 ⊢ 1 ∈ ℕ0
4 repswccat ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 2 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( 𝑆 repeatS 2 ) ++ ( 𝑆 repeatS 1 ) ) = ( 𝑆 repeatS ( 2 + 1 ) ) )
5 2 3 4 mp3an23 ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 repeatS 2 ) ++ ( 𝑆 repeatS 1 ) ) = ( 𝑆 repeatS ( 2 + 1 ) ) )
6 repsw2 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 2 ) = ⟨“ 𝑆 𝑆 ”⟩ )
7 repsw1 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 1 ) = ⟨“ 𝑆 ”⟩ )
8 6 7 oveq12d ⊢ ( 𝑆 ∈ 𝑉 → ( ( 𝑆 repeatS 2 ) ++ ( 𝑆 repeatS 1 ) ) = ( ⟨“ 𝑆 𝑆 ”⟩ ++ ⟨“ 𝑆 ”⟩ ) )
9 2p1e3 ⊢ ( 2 + 1 ) = 3
10 9 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( 2 + 1 ) = 3 )
11 10 oveq2d ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS ( 2 + 1 ) ) = ( 𝑆 repeatS 3 ) )
12 5 8 11 3eqtr3d ⊢ ( 𝑆 ∈ 𝑉 → ( ⟨“ 𝑆 𝑆 ”⟩ ++ ⟨“ 𝑆 ”⟩ ) = ( 𝑆 repeatS 3 ) )
13 1 12 eqtr2id ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 3 ) = ⟨“ 𝑆 𝑆 𝑆 ”⟩ )