Theorem pfx1s2

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

	Ref	Expression
Assertion	pfx1s2	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩\mathrm{prefix}1=⟨“A”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s2cl	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩\in \mathrm{Word}V$$
2		2re	$$⊢2\in ℝ$$
3	2	leidi	$$⊢2\le 2$$
4		s2len	$$⊢\left|⟨“AB”⟩\right|=2$$
5	3 4	breqtrri	$$⊢2\le \left|⟨“AB”⟩\right|$$
6		wrdlenge2n0	$$⊢\left(⟨“AB”⟩\in \mathrm{Word}V\wedge 2\le \left|⟨“AB”⟩\right|\right)\to ⟨“AB”⟩\ne \varnothing$$
7	5 6	mpan2	$$⊢⟨“AB”⟩\in \mathrm{Word}V\to ⟨“AB”⟩\ne \varnothing$$
8		pfx1	$$⊢\left(⟨“AB”⟩\in \mathrm{Word}V\wedge ⟨“AB”⟩\ne \varnothing \right)\to ⟨“AB”⟩\mathrm{prefix}1=⟨“⟨“AB”⟩\left(0\right)”⟩$$
9	1 7 8	syl2anc2	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩\mathrm{prefix}1=⟨“⟨“AB”⟩\left(0\right)”⟩$$
10		s2fv0	$$⊢A\in V\to ⟨“AB”⟩\left(0\right)=A$$
11	10	adantr	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩\left(0\right)=A$$
12	11	s1eqd	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“⟨“AB”⟩\left(0\right)”⟩=⟨“A”⟩$$
13	9 12	eqtrd	$$⊢\left(A\in V\wedge B\in V\right)\to ⟨“AB”⟩\mathrm{prefix}1=⟨“A”⟩$$