# Metamath Proof Explorer

## Theorem lmat22e22

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 lmat22e22 ${⊢}{\phi }\to 2{M}2={D}$

### 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 6 nnrei ${⊢}2\in ℝ$
16 15 leidi ${⊢}2\le 2$
17 1p1e2 ${⊢}1+1=2$
18 s2cli ${⊢}⟨“{C}{D}”⟩\in \mathrm{Word}\mathrm{V}$
19 s2fv1 ${⊢}⟨“{C}{D}”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
20 18 19 ax-mp ${⊢}⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
21 s2fv1 ${⊢}{D}\in {V}\to ⟨“{C}{D}”⟩\left(1\right)={D}$
22 5 21 syl ${⊢}{\phi }\to ⟨“{C}{D}”⟩\left(1\right)={D}$
23 1 7 10 12 13 14 14 16 16 17 17 20 22 lmatfvlem ${⊢}{\phi }\to 2{M}2={D}$