Metamath Proof Explorer

Theorem repsw3

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

Ref Expression
Assertion repsw3 
|- ( S e. V -> ( S repeatS 3 ) = <" S S S "> )

Proof

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