# 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}=\mathrm{litMat}\left(⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\right)$
lmat22.a ${⊢}{\phi }\to {A}\in {V}$
lmat22.b ${⊢}{\phi }\to {B}\in {V}$
lmat22.c ${⊢}{\phi }\to {C}\in {V}$
lmat22.d ${⊢}{\phi }\to {D}\in {V}$
Assertion lmat22e21 ${⊢}{\phi }\to 2{M}1={C}$

### Proof

Step Hyp Ref Expression
1 lmat22.m ${⊢}{M}=\mathrm{litMat}\left(⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\right)$
2 lmat22.a ${⊢}{\phi }\to {A}\in {V}$
3 lmat22.b ${⊢}{\phi }\to {B}\in {V}$
4 lmat22.c ${⊢}{\phi }\to {C}\in {V}$
5 lmat22.d ${⊢}{\phi }\to {D}\in {V}$
6 2nn ${⊢}2\in ℕ$
7 6 a1i ${⊢}{\phi }\to 2\in ℕ$
8 2 3 s2cld ${⊢}{\phi }\to ⟨“{A}{B}”⟩\in \mathrm{Word}{V}$
9 4 5 s2cld ${⊢}{\phi }\to ⟨“{C}{D}”⟩\in \mathrm{Word}{V}$
10 8 9 s2cld ${⊢}{\phi }\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\in \mathrm{Word}\mathrm{Word}{V}$
11 s2len ${⊢}\left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\right|=2$
12 11 a1i ${⊢}{\phi }\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\right|=2$
13 1 2 3 4 5 lmat22lem ${⊢}\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$
14 1nn0 ${⊢}1\in {ℕ}_{0}$
15 0nn0 ${⊢}0\in {ℕ}_{0}$
16 6 nnrei ${⊢}2\in ℝ$
17 16 leidi ${⊢}2\le 2$
18 1le2 ${⊢}1\le 2$
19 1p1e2 ${⊢}1+1=2$
20 0p1e1 ${⊢}0+1=1$
21 s2cli ${⊢}⟨“{C}{D}”⟩\in \mathrm{Word}\mathrm{V}$
22 s2fv1 ${⊢}⟨“{C}{D}”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
23 21 22 ax-mp ${⊢}⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
24 s2fv0 ${⊢}{C}\in {V}\to ⟨“{C}{D}”⟩\left(0\right)={C}$
25 4 24 syl ${⊢}{\phi }\to ⟨“{C}{D}”⟩\left(0\right)={C}$
26 1 7 10 12 13 14 15 17 18 19 20 23 25 lmatfvlem ${⊢}{\phi }\to 2{M}1={C}$