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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({N}\right)={X}$

Proof

Step Hyp Ref Expression
1 ccatws1cl ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {X}\in {V}\right)\to {W}\mathrm{++}⟨“{X}”⟩\in \mathrm{Word}{V}$
2 1 3adant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to {W}\mathrm{++}⟨“{X}”⟩\in \mathrm{Word}{V}$
3 lencl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in {ℕ}_{0}$
4 fzonn0p1 ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|\in \left(0..^\left|{W}\right|+1\right)$
5 3 4 syl ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\right|\in \left(0..^\left|{W}\right|+1\right)$
6 5 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to \left|{W}\right|\in \left(0..^\left|{W}\right|+1\right)$
7 simpr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to \left|{W}\right|={N}$
8 7 eqcomd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to {N}=\left|{W}\right|$
9 ccatws1len ${⊢}{W}\in \mathrm{Word}{V}\to \left|{W}\mathrm{++}⟨“{X}”⟩\right|=\left|{W}\right|+1$
10 9 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to \left|{W}\mathrm{++}⟨“{X}”⟩\right|=\left|{W}\right|+1$
11 10 oveq2d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to \left(0..^\left|{W}\mathrm{++}⟨“{X}”⟩\right|\right)=\left(0..^\left|{W}\right|+1\right)$
12 6 8 11 3eltr4d ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\right)\to {N}\in \left(0..^\left|{W}\mathrm{++}⟨“{X}”⟩\right|\right)$
13 12 3adant3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to {N}\in \left(0..^\left|{W}\mathrm{++}⟨“{X}”⟩\right|\right)$
14 ccats1val1 ${⊢}\left({W}\mathrm{++}⟨“{X}”⟩\in \mathrm{Word}{V}\wedge {N}\in \left(0..^\left|{W}\mathrm{++}⟨“{X}”⟩\right|\right)\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({N}\right)=\left({W}\mathrm{++}⟨“{X}”⟩\right)\left({N}\right)$
15 2 13 14 syl2anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({N}\right)=\left({W}\mathrm{++}⟨“{X}”⟩\right)\left({N}\right)$
16 simp1 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to {W}\in \mathrm{Word}{V}$
17 simp3 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to {X}\in {V}$
18 eqcom ${⊢}\left|{W}\right|={N}↔{N}=\left|{W}\right|$
19 18 biimpi ${⊢}\left|{W}\right|={N}\to {N}=\left|{W}\right|$
20 19 3ad2ant2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to {N}=\left|{W}\right|$
21 ccats1val2 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {X}\in {V}\wedge {N}=\left|{W}\right|\right)\to \left({W}\mathrm{++}⟨“{X}”⟩\right)\left({N}\right)={X}$
22 16 17 20 21 syl3anc ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to \left({W}\mathrm{++}⟨“{X}”⟩\right)\left({N}\right)={X}$
23 15 22 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge \left|{W}\right|={N}\wedge {X}\in {V}\right)\to \left(\left({W}\mathrm{++}⟨“{X}”⟩\right)\mathrm{++}⟨“{Y}”⟩\right)\left({N}\right)={X}$