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 ⊢ S ∈ V → S repeatS 3 = ⟨“ SSS ”⟩

Proof

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