Metamath Proof Explorer

Theorem ccatw2s1p1

Description: Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof shortened by AV, 1-May-2020) (Revised by AV, 1-May-2020) (Revised by AV, 29-Jan-2024)

Ref Expression
Assertion ccatw2s1p1 
|- ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = X )

Proof

Step Hyp Ref Expression
1 ccatws1cl 
 |-  ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
2 1 3adant2 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 fzonn0p1 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ..^ ( ( # ` W ) + 1 ) ) )
5 3 4 syl 
 |-  ( W e. Word V -> ( # ` W ) e. ( 0 ..^ ( ( # ` W ) + 1 ) ) )
6 5 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> ( # ` W ) e. ( 0 ..^ ( ( # ` W ) + 1 ) ) )
7 simpr 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> ( # ` W ) = N )
8 7 eqcomd 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> N = ( # ` W ) )
9 ccatws1len 
 |-  ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
10 9 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
11 10 oveq2d 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> ( 0 ..^ ( # ` ( W ++ <" X "> ) ) ) = ( 0 ..^ ( ( # ` W ) + 1 ) ) )
12 6 8 11 3eltr4d 
 |-  ( ( W e. Word V /\ ( # ` W ) = N ) -> N e. ( 0 ..^ ( # ` ( W ++ <" X "> ) ) ) )
13 12 3adant3 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> N e. ( 0 ..^ ( # ` ( W ++ <" X "> ) ) ) )
14 ccats1val1 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ N e. ( 0 ..^ ( # ` ( W ++ <" X "> ) ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = ( ( W ++ <" X "> ) ` N ) )
15 2 13 14 syl2anc 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = ( ( W ++ <" X "> ) ` N ) )
16 simp1 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> W e. Word V )
17 simp3 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> X e. V )
18 eqcom 
 |-  ( ( # ` W ) = N <-> N = ( # ` W ) )
19 18 biimpi 
 |-  ( ( # ` W ) = N -> N = ( # ` W ) )
20 19 3ad2ant2 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> N = ( # ` W ) )
21 ccats1val2 
 |-  ( ( W e. Word V /\ X e. V /\ N = ( # ` W ) ) -> ( ( W ++ <" X "> ) ` N ) = X )
22 16 17 20 21 syl3anc 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> ( ( W ++ <" X "> ) ` N ) = X )
23 15 22 eqtrd 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ X e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = X )