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

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 1z ⊢ 1 ∈ ℤ
6 2z ⊢ 2 ∈ ℤ
7 1lt2 ⊢ 1 < 2
8 fzolb ⊢ 1 ∈ 1 ..^ 2 ↔ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 < 2
9 5 6 7 8 mpbir3an ⊢ 1 ∈ 1 ..^ 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 ⊢ X ∈ V ∧ Y ∈ V → 1 ∈ ⟨“ X ”⟩ ..^ ⟨“ X ”⟩ + ⟨“ Y ”⟩
18 ccatval2 ⊢ ⟨“ X ”⟩ ∈ Word V ∧ ⟨“ Y ”⟩ ∈ Word V ∧ 1 ∈ ⟨“ X ”⟩ ..^ ⟨“ X ”⟩ + ⟨“ Y ”⟩ → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 1 = ⟨“ Y ”⟩ ⁡ 1 − ⟨“ X ”⟩
19 2 4 17 18 syl3anc ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 1 = ⟨“ Y ”⟩ ⁡ 1 − ⟨“ X ”⟩
20 10 oveq2i ⊢ 1 − ⟨“ X ”⟩ = 1 − 1
21 1m1e0 ⊢ 1 − 1 = 0
22 20 21 eqtri ⊢ 1 − ⟨“ X ”⟩ = 0
23 22 a1i ⊢ Y ∈ V → 1 − ⟨“ X ”⟩ = 0
24 23 fveq2d ⊢ Y ∈ V → ⟨“ Y ”⟩ ⁡ 1 − ⟨“ X ”⟩ = ⟨“ Y ”⟩ ⁡ 0
25 s1fv ⊢ Y ∈ V → ⟨“ Y ”⟩ ⁡ 0 = Y
26 24 25 eqtrd ⊢ Y ∈ V → ⟨“ Y ”⟩ ⁡ 1 − ⟨“ X ”⟩ = Y
27 26 adantl ⊢ X ∈ V ∧ Y ∈ V → ⟨“ Y ”⟩ ⁡ 1 − ⟨“ X ”⟩ = Y
28 19 27 eqtrd ⊢ X ∈ V ∧ Y ∈ V → ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 1 = Y