This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatrid

Description: Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatrid 
|- ( S e. Word B -> ( S ++ (/) ) = S )

Proof

Step Hyp Ref Expression
1 wrd0 
 |-  (/) e. Word B
2 ccatvalfn 
 |-  ( ( S e. Word B /\ (/) e. Word B ) -> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
3 1 2 mpan2 
 |-  ( S e. Word B -> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
4 hash0 
 |-  ( # ` (/) ) = 0
5 4 oveq2i 
 |-  ( ( # ` S ) + ( # ` (/) ) ) = ( ( # ` S ) + 0 )
6 lencl 
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
7 6 nn0cnd 
 |-  ( S e. Word B -> ( # ` S ) e. CC )
8 7 addridd 
 |-  ( S e. Word B -> ( ( # ` S ) + 0 ) = ( # ` S ) )
9 5 8 eqtr2id 
 |-  ( S e. Word B -> ( # ` S ) = ( ( # ` S ) + ( # ` (/) ) ) )
10 9 oveq2d 
 |-  ( S e. Word B -> ( 0 ..^ ( # ` S ) ) = ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) )
11 10 fneq2d 
 |-  ( S e. Word B -> ( ( S ++ (/) ) Fn ( 0 ..^ ( # ` S ) ) <-> ( S ++ (/) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` (/) ) ) ) ) )
12 3 11 mpbird 
 |-  ( S e. Word B -> ( S ++ (/) ) Fn ( 0 ..^ ( # ` S ) ) )
13 wrdfn 
 |-  ( S e. Word B -> S Fn ( 0 ..^ ( # ` S ) ) )
14 ccatval1 
 |-  ( ( S e. Word B /\ (/) e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ (/) ) ` x ) = ( S ` x ) )
15 1 14 mp3an2 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ (/) ) ` x ) = ( S ` x ) )
16 12 13 15 eqfnfvd 
 |-  ( S e. Word B -> ( S ++ (/) ) = S )