Theorem repsw2

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

	Ref	Expression
Assertion	repsw2	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 repeatS 2 ) = ⟨“ 𝑆 𝑆 ”⟩ )

Proof

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