This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfx1s2

Description: The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Assertion pfx1s2 ⊢ A ∈ V ∧ B ∈ V → ⟨“ AB ”⟩ prefix 1 = ⟨“ A ”⟩

Proof

Step Hyp Ref Expression
1 s2cl ⊢ A ∈ V ∧ B ∈ V → ⟨“ AB ”⟩ ∈ Word V
2 2re ⊢ 2 ∈ ℝ
3 2 leidi ⊢ 2 ≤ 2
4 s2len ⊢ ⟨“ AB ”⟩ = 2
5 3 4 breqtrri ⊢ 2 ≤ ⟨“ AB ”⟩
6 wrdlenge2n0 ⊢ ⟨“ AB ”⟩ ∈ Word V ∧ 2 ≤ ⟨“ AB ”⟩ → ⟨“ AB ”⟩ ≠ ∅
7 5 6 mpan2 ⊢ ⟨“ AB ”⟩ ∈ Word V → ⟨“ AB ”⟩ ≠ ∅
8 pfx1 ⊢ ⟨“ AB ”⟩ ∈ Word V ∧ ⟨“ AB ”⟩ ≠ ∅ → ⟨“ AB ”⟩ prefix 1 = ⟨“ ⟨“ AB ”⟩ ⁡ 0 ”⟩
9 1 7 8 syl2anc2 ⊢ A ∈ V ∧ B ∈ V → ⟨“ AB ”⟩ prefix 1 = ⟨“ ⟨“ AB ”⟩ ⁡ 0 ”⟩
10 s2fv0 ⊢ A ∈ V → ⟨“ AB ”⟩ ⁡ 0 = A
11 10 adantr ⊢ A ∈ V ∧ B ∈ V → ⟨“ AB ”⟩ ⁡ 0 = A
12 11 s1eqd ⊢ A ∈ V ∧ B ∈ V → ⟨“ ⟨“ AB ”⟩ ⁡ 0 ”⟩ = ⟨“ A ”⟩
13 9 12 eqtrd ⊢ A ∈ V ∧ B ∈ V → ⟨“ AB ”⟩ prefix 1 = ⟨“ A ”⟩