Metamath Proof Explorer

Theorem ccats1val2

Description: Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Proof shortened by Alexander van der Vekens, 14-Oct-2018)

Ref Expression
Assertion ccats1val2 
|- ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( ( W ++ <" S "> ) ` I ) = S )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> W e. Word V )
2 s1cl 
 |-  ( S e. V -> <" S "> e. Word V )
3 2 3ad2ant2 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> <" S "> e. Word V )
4 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
5 4 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
6 elfzomin 
 |-  ( ( # ` W ) e. ZZ -> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + 1 ) ) )
7 5 6 syl 
 |-  ( W e. Word V -> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + 1 ) ) )
8 s1len 
 |-  ( # ` <" S "> ) = 1
9 8 oveq2i 
 |-  ( ( # ` W ) + ( # ` <" S "> ) ) = ( ( # ` W ) + 1 )
10 9 oveq2i 
 |-  ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) = ( ( # ` W ) ..^ ( ( # ` W ) + 1 ) )
11 7 10 eleqtrrdi 
 |-  ( W e. Word V -> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) )
12 11 adantr 
 |-  ( ( W e. Word V /\ I = ( # ` W ) ) -> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) )
13 eleq1 
 |-  ( I = ( # ` W ) -> ( I e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) <-> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) ) )
14 13 adantl 
 |-  ( ( W e. Word V /\ I = ( # ` W ) ) -> ( I e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) <-> ( # ` W ) e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) ) )
15 12 14 mpbird 
 |-  ( ( W e. Word V /\ I = ( # ` W ) ) -> I e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) )
16 15 3adant2 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> I e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) )
17 ccatval2 
 |-  ( ( W e. Word V /\ <" S "> e. Word V /\ I e. ( ( # ` W ) ..^ ( ( # ` W ) + ( # ` <" S "> ) ) ) ) -> ( ( W ++ <" S "> ) ` I ) = ( <" S "> ` ( I - ( # ` W ) ) ) )
18 1 3 16 17 syl3anc 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( ( W ++ <" S "> ) ` I ) = ( <" S "> ` ( I - ( # ` W ) ) ) )
19 oveq1 
 |-  ( I = ( # ` W ) -> ( I - ( # ` W ) ) = ( ( # ` W ) - ( # ` W ) ) )
20 19 3ad2ant3 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( I - ( # ` W ) ) = ( ( # ` W ) - ( # ` W ) ) )
21 4 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
22 21 subidd 
 |-  ( W e. Word V -> ( ( # ` W ) - ( # ` W ) ) = 0 )
23 22 3ad2ant1 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( ( # ` W ) - ( # ` W ) ) = 0 )
24 20 23 eqtrd 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( I - ( # ` W ) ) = 0 )
25 24 fveq2d 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( <" S "> ` ( I - ( # ` W ) ) ) = ( <" S "> ` 0 ) )
26 s1fv 
 |-  ( S e. V -> ( <" S "> ` 0 ) = S )
27 26 3ad2ant2 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( <" S "> ` 0 ) = S )
28 18 25 27 3eqtrd 
 |-  ( ( W e. Word V /\ S e. V /\ I = ( # ` W ) ) -> ( ( W ++ <" S "> ) ` I ) = S )