Metamath Proof Explorer

Theorem lmat22lem

Description: Lemma for lmat22e11 and co. (Contributed by Thierry Arnoux, 28-Aug-2020)

Ref Expression
Hypotheses lmat22.m 
|- M = ( litMat ` <" <" A B "> <" C D "> "> )
lmat22.a 
|- ( ph -> A e. V )
lmat22.b 
|- ( ph -> B e. V )
lmat22.c 
|- ( ph -> C e. V )
lmat22.d 
|- ( ph -> D e. V )
Assertion lmat22lem 
|- ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )

Proof

Step Hyp Ref Expression
1 lmat22.m 
 |-  M = ( litMat ` <" <" A B "> <" C D "> "> )
2 lmat22.a 
 |-  ( ph -> A e. V )
3 lmat22.b 
 |-  ( ph -> B e. V )
4 lmat22.c 
 |-  ( ph -> C e. V )
5 lmat22.d 
 |-  ( ph -> D e. V )
6 simpr 
 |-  ( ( ph /\ i = 0 ) -> i = 0 )
7 6 fveq2d 
 |-  ( ( ph /\ i = 0 ) -> ( <" <" A B "> <" C D "> "> ` i ) = ( <" <" A B "> <" C D "> "> ` 0 ) )
8 2 3 s2cld 
 |-  ( ph -> <" A B "> e. Word V )
9 s2fv0 
 |-  ( <" A B "> e. Word V -> ( <" <" A B "> <" C D "> "> ` 0 ) = <" A B "> )
10 8 9 syl 
 |-  ( ph -> ( <" <" A B "> <" C D "> "> ` 0 ) = <" A B "> )
11 10 adantr 
 |-  ( ( ph /\ i = 0 ) -> ( <" <" A B "> <" C D "> "> ` 0 ) = <" A B "> )
12 7 11 eqtrd 
 |-  ( ( ph /\ i = 0 ) -> ( <" <" A B "> <" C D "> "> ` i ) = <" A B "> )
13 12 fveq2d 
 |-  ( ( ph /\ i = 0 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = ( # ` <" A B "> ) )
14 s2len 
 |-  ( # ` <" A B "> ) = 2
15 13 14 eqtrdi 
 |-  ( ( ph /\ i = 0 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
16 15 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ 2 ) ) /\ i = 0 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
17 simpr 
 |-  ( ( ph /\ i = 1 ) -> i = 1 )
18 17 fveq2d 
 |-  ( ( ph /\ i = 1 ) -> ( <" <" A B "> <" C D "> "> ` i ) = ( <" <" A B "> <" C D "> "> ` 1 ) )
19 4 5 s2cld 
 |-  ( ph -> <" C D "> e. Word V )
20 s2fv1 
 |-  ( <" C D "> e. Word V -> ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D "> )
21 19 20 syl 
 |-  ( ph -> ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D "> )
22 21 adantr 
 |-  ( ( ph /\ i = 1 ) -> ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D "> )
23 18 22 eqtrd 
 |-  ( ( ph /\ i = 1 ) -> ( <" <" A B "> <" C D "> "> ` i ) = <" C D "> )
24 23 fveq2d 
 |-  ( ( ph /\ i = 1 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = ( # ` <" C D "> ) )
25 s2len 
 |-  ( # ` <" C D "> ) = 2
26 24 25 eqtrdi 
 |-  ( ( ph /\ i = 1 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
27 26 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ 2 ) ) /\ i = 1 ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
28 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
29 28 eleq2i 
 |-  ( i e. ( 0 ..^ 2 ) <-> i e. { 0 , 1 } )
30 vex 
 |-  i e. _V
31 30 elpr 
 |-  ( i e. { 0 , 1 } <-> ( i = 0 \/ i = 1 ) )
32 29 31 bitri 
 |-  ( i e. ( 0 ..^ 2 ) <-> ( i = 0 \/ i = 1 ) )
33 32 biimpi 
 |-  ( i e. ( 0 ..^ 2 ) -> ( i = 0 \/ i = 1 ) )
34 33 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( i = 0 \/ i = 1 ) )
35 16 27 34 mpjaodan 
 |-  ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )