Theorem ccatw2s1p1OLD

Description: Obsolete version of ccatw2s1p1 as of 29-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ccatw2s1p1OLD	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y 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	ad2ant2r	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y 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	adantr	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y 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 /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = ( ( W ++ <" X "> ) ` N ) )
16		simpll	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> W e. Word V )
17		simprl	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> X e. V )
18		eqcom	|- ( ( # ` W ) = N <-> N = ( # ` W ) )
19	18	biimpi	|- ( ( # ` W ) = N -> N = ( # ` W ) )
20	19	ad2antlr	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y 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 /\ Y e. V ) ) -> ( ( W ++ <" X "> ) ` N ) = X )
23	15 22	eqtrd	|- ( ( ( W e. Word V /\ ( # ` W ) = N ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` N ) = X )