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 )