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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ 𝐴 ”⟩ )

Proof

Step Hyp Ref Expression
1 s2cl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 )
2 2re ⊢ 2 ∈ ℝ
3 2 leidi ⊢ 2 ≤ 2
4 s2len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
5 3 4 breqtrri ⊢ 2 ≤ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ )
6 wrdlenge2n0 ⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) → ⟨“ 𝐴 𝐵 ”⟩ ≠ ∅ )
7 5 6 mpan2 ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 → ⟨“ 𝐴 𝐵 ”⟩ ≠ ∅ )
8 pfx1 ⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝐴 𝐵 ”⟩ ≠ ∅ ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) ”⟩ )
9 1 7 8 syl2anc2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) ”⟩ )
10 s2fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 )
11 10 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) = 𝐴 )
12 11 s1eqd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ⟨“ ( ⟨“ 𝐴 𝐵 ”⟩ ‘ 0 ) ”⟩ = ⟨“ 𝐴 ”⟩ )
13 9 12 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ⟨“ 𝐴 𝐵 ”⟩ prefix 1 ) = ⟨“ 𝐴 ”⟩ )