Theorem repsw3

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

	Ref	Expression
Assertion	repsw3	$$⊢S\in V\to S\mathrm{repeatS}3=⟨“SSS”⟩$$

Proof

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