Theorem repsw2

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

	Ref	Expression
Assertion	repsw2	$$⊢S\in V\to S\mathrm{repeatS}2=⟨“SS”⟩$$

Proof

Step	Hyp	Ref	Expression
1		df-s2	$$⊢⟨“SS”⟩=⟨“S”⟩\mathrm{++}⟨“S”⟩$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		repswccat	$$⊢\left(S\in V\wedge 1\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \left(S\mathrm{repeatS}1\right)\mathrm{++}\left(S\mathrm{repeatS}1\right)=S\mathrm{repeatS}\left(1+1\right)$$
4	2 2 3	mp3an23	$$⊢S\in V\to \left(S\mathrm{repeatS}1\right)\mathrm{++}\left(S\mathrm{repeatS}1\right)=S\mathrm{repeatS}\left(1+1\right)$$
5		repsw1	$$⊢S\in V\to S\mathrm{repeatS}1=⟨“S”⟩$$
6	5 5	oveq12d	$$⊢S\in V\to \left(S\mathrm{repeatS}1\right)\mathrm{++}\left(S\mathrm{repeatS}1\right)=⟨“S”⟩\mathrm{++}⟨“S”⟩$$
7		1p1e2	$$⊢1+1=2$$
8	7	a1i	$$⊢S\in V\to 1+1=2$$
9	8	oveq2d	$$⊢S\in V\to S\mathrm{repeatS}\left(1+1\right)=S\mathrm{repeatS}2$$
10	4 6 9	3eqtr3d	$$⊢S\in V\to ⟨“S”⟩\mathrm{++}⟨“S”⟩=S\mathrm{repeatS}2$$
11	1 10	eqtr2id	$$⊢S\in V\to S\mathrm{repeatS}2=⟨“SS”⟩$$