# Metamath Proof Explorer

## Theorem lmat22e21

Description: Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-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 lmat22e21
`|- ( ph -> ( 2 M 1 ) = C )`

### 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 1nn0
` |-  1 e. NN0`
15 0nn0
` |-  0 e. NN0`
16 6 nnrei
` |-  2 e. RR`
17 16 leidi
` |-  2 <_ 2`
18 1le2
` |-  1 <_ 2`
19 1p1e2
` |-  ( 1 + 1 ) = 2`
20 0p1e1
` |-  ( 0 + 1 ) = 1`
21 s2cli
` |-  <" C D "> e. Word _V`
22 s2fv1
` |-  ( <" C D "> e. Word _V -> ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D "> )`
23 21 22 ax-mp
` |-  ( <" <" A B "> <" C D "> "> ` 1 ) = <" C D ">`
24 s2fv0
` |-  ( C e. V -> ( <" C D "> ` 0 ) = C )`
25 4 24 syl
` |-  ( ph -> ( <" C D "> ` 0 ) = C )`
26 1 7 10 12 13 14 15 17 18 19 20 23 25 lmatfvlem
` |-  ( ph -> ( 2 M 1 ) = C )`