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 ) = ⟨“ 𝐴 ”⟩ )