Metamath Proof Explorer


Theorem ccat2s1p1OLD

Description: Obsolete version of ccat2s1p1 as of 20-Jan-2024. Extract the first 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 ccat2s1p1OLD X V Y V ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X

Proof

Step Hyp Ref Expression
1 s1cl X V ⟨“ X ”⟩ Word V
2 1 adantr X V Y V ⟨“ X ”⟩ Word V
3 s1cl Y V ⟨“ Y ”⟩ Word V
4 3 adantl X V Y V ⟨“ Y ”⟩ Word V
5 s1len ⟨“ X ”⟩ = 1
6 5 a1i X V ⟨“ X ”⟩ = 1
7 1nn 1
8 6 7 eqeltrdi X V ⟨“ X ”⟩
9 lbfzo0 0 0 ..^ ⟨“ X ”⟩ ⟨“ X ”⟩
10 8 9 sylibr X V 0 0 ..^ ⟨“ X ”⟩
11 10 adantr X V Y V 0 0 ..^ ⟨“ X ”⟩
12 ccatval1OLD ⟨“ X ”⟩ Word V ⟨“ Y ”⟩ Word V 0 0 ..^ ⟨“ X ”⟩ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = ⟨“ X ”⟩ 0
13 2 4 11 12 syl3anc X V Y V ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = ⟨“ X ”⟩ 0
14 s1fv X V ⟨“ X ”⟩ 0 = X
15 14 adantr X V Y V ⟨“ X ”⟩ 0 = X
16 13 15 eqtrd X V Y V ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X