Metamath Proof Explorer

Theorem lmat22e11

Description: Entry of a 2x2 literal matrix. (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 lmat22e11 
|- ( ph -> ( 1 M 1 ) = A )

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 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ph -> 2 e. NN )
8 2 3 s2cld 
 |-  ( ph -> <" A B "> e. Word V )
9 4 5 s2cld 
 |-  ( ph -> <" C D "> e. Word V )
10 8 9 s2cld 
 |-  ( ph -> <" <" A B "> <" C D "> "> e. Word Word V )
11 s2len 
 |-  ( # ` <" <" A B "> <" C D "> "> ) = 2
12 11 a1i 
 |-  ( ph -> ( # ` <" <" A B "> <" C D "> "> ) = 2 )
13 1 2 3 4 5 lmat22lem 
 |-  ( ( ph /\ i e. ( 0 ..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
14 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
15 eluzfz1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... 2 ) )
16 14 15 ax-mp 
 |-  1 e. ( 1 ... 2 )
17 16 a1i 
 |-  ( ph -> 1 e. ( 1 ... 2 ) )
18 1 7 10 12 13 17 17 lmatfval 
 |-  ( ph -> ( 1 M 1 ) = ( ( <" <" A B "> <" C D "> "> ` ( 1 - 1 ) ) ` ( 1 - 1 ) ) )
19 1m1e0 
 |-  ( 1 - 1 ) = 0
20 19 fveq2i 
 |-  ( <" <" A B "> <" C D "> "> ` ( 1 - 1 ) ) = ( <" <" A B "> <" C D "> "> ` 0 )
21 s2fv0 
 |-  ( <" A B "> e. Word V -> ( <" <" A B "> <" C D "> "> ` 0 ) = <" A B "> )
22 8 21 syl 
 |-  ( ph -> ( <" <" A B "> <" C D "> "> ` 0 ) = <" A B "> )
23 20 22 syl5eq 
 |-  ( ph -> ( <" <" A B "> <" C D "> "> ` ( 1 - 1 ) ) = <" A B "> )
24 19 a1i 
 |-  ( ph -> ( 1 - 1 ) = 0 )
25 23 24 fveq12d 
 |-  ( ph -> ( ( <" <" A B "> <" C D "> "> ` ( 1 - 1 ) ) ` ( 1 - 1 ) ) = ( <" A B "> ` 0 ) )
26 s2fv0 
 |-  ( A e. V -> ( <" A B "> ` 0 ) = A )
27 2 26 syl 
 |-  ( ph -> ( <" A B "> ` 0 ) = A )
28 18 25 27 3eqtrd 
 |-  ( ph -> ( 1 M 1 ) = A )