Metamath Proof Explorer

Theorem ccat2s1p2

Description: Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by JJ, 20-Jan-2024)

Ref Expression
Assertion ccat2s1p2 ⊢Y∈V→⟨“X”⟩++⟨“Y”⟩⁡1=Y

Proof

Step Hyp Ref Expression
1 s1cli ⊢⟨“X”⟩∈WordV
2 s1cli ⊢⟨“Y”⟩∈WordV
3 1z ⊢1∈ℤ
4 2z ⊢2∈ℤ
5 1lt2 ⊢1<2
6 fzolb ⊢1∈1..^2↔1∈ℤ∧2∈ℤ∧1<2
7 3 4 5 6 mpbir3an ⊢1∈1..^2
8 s1len ⊢⟨“X”⟩=1
9 s1len ⊢⟨“Y”⟩=1
10 8 9 oveq12i ⊢⟨“X”⟩+⟨“Y”⟩=1+1
11 1p1e2 ⊢1+1=2
12 10 11 eqtri ⊢⟨“X”⟩+⟨“Y”⟩=2
13 8 12 oveq12i ⊢⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩=1..^2
14 7 13 eleqtrri ⊢1∈⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩
15 ccatval2 ⊢⟨“X”⟩∈WordV∧⟨“Y”⟩∈WordV∧1∈⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩→⟨“X”⟩++⟨“Y”⟩⁡1=⟨“Y”⟩⁡1−⟨“X”⟩
16 1 2 14 15 mp3an ⊢⟨“X”⟩++⟨“Y”⟩⁡1=⟨“Y”⟩⁡1−⟨“X”⟩
17 8 oveq2i ⊢1−⟨“X”⟩=1−1
18 1m1e0 ⊢1−1=0
19 17 18 eqtri ⊢1−⟨“X”⟩=0
20 19 fveq2i ⊢⟨“Y”⟩⁡1−⟨“X”⟩=⟨“Y”⟩⁡0
21 16 20 eqtri ⊢⟨“X”⟩++⟨“Y”⟩⁡1=⟨“Y”⟩⁡0
22 s1fv ⊢Y∈V→⟨“Y”⟩⁡0=Y
23 21 22 eqtrid ⊢Y∈V→⟨“X”⟩++⟨“Y”⟩⁡1=Y