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 
|- ( S e. V -> ( S repeatS 2 ) = <" S S "> )

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" S S "> = ( <" S "> ++ <" S "> )
2 1nn0 
 |-  1 e. NN0
3 repswccat 
 |-  ( ( S e. V /\ 1 e. NN0 /\ 1 e. NN0 ) -> ( ( S repeatS 1 ) ++ ( S repeatS 1 ) ) = ( S repeatS ( 1 + 1 ) ) )
4 2 2 3 mp3an23 
 |-  ( S e. V -> ( ( S repeatS 1 ) ++ ( S repeatS 1 ) ) = ( S repeatS ( 1 + 1 ) ) )
5 repsw1 
 |-  ( S e. V -> ( S repeatS 1 ) = <" S "> )
6 5 5 oveq12d 
 |-  ( S e. V -> ( ( S repeatS 1 ) ++ ( S repeatS 1 ) ) = ( <" S "> ++ <" S "> ) )
7 1p1e2 
 |-  ( 1 + 1 ) = 2
8 7 a1i 
 |-  ( S e. V -> ( 1 + 1 ) = 2 )
9 8 oveq2d 
 |-  ( S e. V -> ( S repeatS ( 1 + 1 ) ) = ( S repeatS 2 ) )
10 4 6 9 3eqtr3d 
 |-  ( S e. V -> ( <" S "> ++ <" S "> ) = ( S repeatS 2 ) )
11 1 10 eqtr2id 
 |-  ( S e. V -> ( S repeatS 2 ) = <" S S "> )