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 ”⟩ ∈ Word V
2 s1cli ⊢ ⟨“ Y ”⟩ ∈ Word V
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 ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V ∧ 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 syl5eq ⊢ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 1 = Y