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 ”⟩