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 ) = ⟨“ 𝑆 𝑆 𝑆 ”⟩ )