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

Metamath Proof Explorer

Theorem ccatlid

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

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

Proof

Step Hyp Ref Expression
1 wrd0 
 |-  (/) e. Word B
2 ccatvalfn 
 |-  ( ( (/) e. Word B /\ S e. Word B ) -> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
3 1 2 mpan 
 |-  ( S e. Word B -> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
4 hash0 
 |-  ( # ` (/) ) = 0
5 4 oveq1i 
 |-  ( ( # ` (/) ) + ( # ` S ) ) = ( 0 + ( # ` S ) )
6 lencl 
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
7 6 nn0cnd 
 |-  ( S e. Word B -> ( # ` S ) e. CC )
8 7 addlidd 
 |-  ( S e. Word B -> ( 0 + ( # ` S ) ) = ( # ` S ) )
9 5 8 eqtrid 
 |-  ( S e. Word B -> ( ( # ` (/) ) + ( # ` S ) ) = ( # ` S ) )
10 9 eqcomd 
 |-  ( S e. Word B -> ( # ` S ) = ( ( # ` (/) ) + ( # ` S ) ) )
11 10 oveq2d 
 |-  ( S e. Word B -> ( 0 ..^ ( # ` S ) ) = ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
12 11 fneq2d 
 |-  ( S e. Word B -> ( ( (/) ++ S ) Fn ( 0 ..^ ( # ` S ) ) <-> ( (/) ++ S ) Fn ( 0 ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) )
13 3 12 mpbird 
 |-  ( S e. Word B -> ( (/) ++ S ) Fn ( 0 ..^ ( # ` S ) ) )
14 wrdfn 
 |-  ( S e. Word B -> S Fn ( 0 ..^ ( # ` S ) ) )
15 4 a1i 
 |-  ( S e. Word B -> ( # ` (/) ) = 0 )
16 15 9 oveq12d 
 |-  ( S e. Word B -> ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) = ( 0 ..^ ( # ` S ) ) )
17 16 eleq2d 
 |-  ( S e. Word B -> ( x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) <-> x e. ( 0 ..^ ( # ` S ) ) ) )
18 17 biimpar 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) )
19 ccatval2 
 |-  ( ( (/) e. Word B /\ S e. Word B /\ x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
20 1 19 mp3an1 
 |-  ( ( S e. Word B /\ x e. ( ( # ` (/) ) ..^ ( ( # ` (/) ) + ( # ` S ) ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
21 18 20 syldan 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` ( x - ( # ` (/) ) ) ) )
22 4 oveq2i 
 |-  ( x - ( # ` (/) ) ) = ( x - 0 )
23 elfzoelz 
 |-  ( x e. ( 0 ..^ ( # ` S ) ) -> x e. ZZ )
24 23 adantl 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ZZ )
25 24 zcnd 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> x e. CC )
26 25 subid1d 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - 0 ) = x )
27 22 26 eqtrid 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - ( # ` (/) ) ) = x )
28 27 fveq2d 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` ( x - ( # ` (/) ) ) ) = ( S ` x ) )
29 21 28 eqtrd 
 |-  ( ( S e. Word B /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( (/) ++ S ) ` x ) = ( S ` x ) )
30 13 14 29 eqfnfvd 
 |-  ( S e. Word B -> ( (/) ++ S ) = S )