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

Metamath Proof Explorer

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