Metamath Proof Explorer


Theorem ccat2s1p2OLD

Description: Obsolete version of ccat2s1p2 as of 20-Jan-2024. Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ccat2s1p2OLD XVYV⟨“X”⟩++⟨“Y”⟩1=Y

Proof

Step Hyp Ref Expression
1 s1cl XV⟨“X”⟩WordV
2 1 adantr XVYV⟨“X”⟩WordV
3 s1cl YV⟨“Y”⟩WordV
4 3 adantl XVYV⟨“Y”⟩WordV
5 1z 1
6 2z 2
7 1lt2 1<2
8 fzolb 11..^2121<2
9 5 6 7 8 mpbir3an 11..^2
10 s1len ⟨“X”⟩=1
11 s1len ⟨“Y”⟩=1
12 10 11 oveq12i ⟨“X”⟩+⟨“Y”⟩=1+1
13 1p1e2 1+1=2
14 12 13 eqtri ⟨“X”⟩+⟨“Y”⟩=2
15 10 14 oveq12i ⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩=1..^2
16 9 15 eleqtrri 1⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩
17 16 a1i XVYV1⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩
18 ccatval2 ⟨“X”⟩WordV⟨“Y”⟩WordV1⟨“X”⟩..^⟨“X”⟩+⟨“Y”⟩⟨“X”⟩++⟨“Y”⟩1=⟨“Y”⟩1⟨“X”⟩
19 2 4 17 18 syl3anc XVYV⟨“X”⟩++⟨“Y”⟩1=⟨“Y”⟩1⟨“X”⟩
20 10 oveq2i 1⟨“X”⟩=11
21 1m1e0 11=0
22 20 21 eqtri 1⟨“X”⟩=0
23 22 a1i YV1⟨“X”⟩=0
24 23 fveq2d YV⟨“Y”⟩1⟨“X”⟩=⟨“Y”⟩0
25 s1fv YV⟨“Y”⟩0=Y
26 24 25 eqtrd YV⟨“Y”⟩1⟨“X”⟩=Y
27 26 adantl XVYV⟨“Y”⟩1⟨“X”⟩=Y
28 19 27 eqtrd XVYV⟨“X”⟩++⟨“Y”⟩1=Y