repsw2

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

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

Step	Hyp	Ref	Expression
1		df-s2	$⊢ ⟨“ S S ”⟩ = ⟨“ S ”⟩ ++ ⟨“ S ”⟩$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		repswccat	$⊢ (S \in V \land 1 \in ℕ_{0} \land 1 \in ℕ_{0}) \to (S repeatS 1) ++ (S repeatS 1) = S repeatS (1 + 1)$
4	2 2 3	mp3an23	$⊢ S \in V \to (S repeatS 1) ++ (S repeatS 1) = S repeatS (1 + 1)$
5		repsw1	$⊢ S \in V \to S repeatS 1 = ⟨“ S ”⟩$
6	5 5	oveq12d	$⊢ S \in V \to (S repeatS 1) ++ (S repeatS 1) = ⟨“ S ”⟩ ++ ⟨“ S ”⟩$
7		1p1e2	$⊢ 1 + 1 = 2$
8	7	a1i	$⊢ S \in V \to 1 + 1 = 2$
9	8	oveq2d	$⊢ S \in V \to S repeatS (1 + 1) = S repeatS 2$
10	4 6 9	3eqtr3d	$⊢ S \in V \to ⟨“ S ”⟩ ++ ⟨“ S ”⟩ = S repeatS 2$
11	1 10	eqtr2id	$⊢ S \in V \to S repeatS 2 = ⟨“ S S ”⟩$

Metamath Proof Explorer