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 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 "> )