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 e. V /\ B e. V ) -> ( <" A B "> prefix 1 ) = <" A "> )

Proof

Step	Hyp	Ref	Expression
1		s2cl	|- ( ( A e. V /\ B e. V ) -> <" A B "> e. Word V )
2		2re	|- 2 e. RR
3	2	leidi	|- 2 <_ 2
4		s2len	|- ( # ` <" A B "> ) = 2
5	3 4	breqtrri	|- 2 <_ ( # ` <" A B "> )
6		wrdlenge2n0	|- ( ( <" A B "> e. Word V /\ 2 <_ ( # ` <" A B "> ) ) -> <" A B "> =/= (/) )
7	5 6	mpan2	|- ( <" A B "> e. Word V -> <" A B "> =/= (/) )
8		pfx1	|- ( ( <" A B "> e. Word V /\ <" A B "> =/= (/) ) -> ( <" A B "> prefix 1 ) = <" ( <" A B "> ` 0 ) "> )
9	1 7 8	syl2anc2	|- ( ( A e. V /\ B e. V ) -> ( <" A B "> prefix 1 ) = <" ( <" A B "> ` 0 ) "> )
10		s2fv0	|- ( A e. V -> ( <" A B "> ` 0 ) = A )
11	10	adantr	|- ( ( A e. V /\ B e. V ) -> ( <" A B "> ` 0 ) = A )
12	11	s1eqd	|- ( ( A e. V /\ B e. V ) -> <" ( <" A B "> ` 0 ) "> = <" A "> )
13	9 12	eqtrd	|- ( ( A e. V /\ B e. V ) -> ( <" A B "> prefix 1 ) = <" A "> )