# Metamath Proof Explorer

## Theorem lmat22lem

Description: Lemma for lmat22e11 and co. (Contributed by Thierry Arnoux, 28-Aug-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 lmat22lem ${⊢}\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$

### 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 simpr ${⊢}\left({\phi }\wedge {i}=0\right)\to {i}=0$
7 6 fveq2d ${⊢}\left({\phi }\wedge {i}=0\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)=⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(0\right)$
8 2 3 s2cld ${⊢}{\phi }\to ⟨“{A}{B}”⟩\in \mathrm{Word}{V}$
9 s2fv0 ${⊢}⟨“{A}{B}”⟩\in \mathrm{Word}{V}\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(0\right)=⟨“{A}{B}”⟩$
10 8 9 syl ${⊢}{\phi }\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(0\right)=⟨“{A}{B}”⟩$
11 10 adantr ${⊢}\left({\phi }\wedge {i}=0\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(0\right)=⟨“{A}{B}”⟩$
12 7 11 eqtrd ${⊢}\left({\phi }\wedge {i}=0\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)=⟨“{A}{B}”⟩$
13 12 fveq2d ${⊢}\left({\phi }\wedge {i}=0\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=\left|⟨“{A}{B}”⟩\right|$
14 s2len ${⊢}\left|⟨“{A}{B}”⟩\right|=2$
15 13 14 syl6eq ${⊢}\left({\phi }\wedge {i}=0\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$
16 15 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\wedge {i}=0\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$
17 simpr ${⊢}\left({\phi }\wedge {i}=1\right)\to {i}=1$
18 17 fveq2d ${⊢}\left({\phi }\wedge {i}=1\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)=⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)$
19 4 5 s2cld ${⊢}{\phi }\to ⟨“{C}{D}”⟩\in \mathrm{Word}{V}$
20 s2fv1 ${⊢}⟨“{C}{D}”⟩\in \mathrm{Word}{V}\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
21 19 20 syl ${⊢}{\phi }\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
22 21 adantr ${⊢}\left({\phi }\wedge {i}=1\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left(1\right)=⟨“{C}{D}”⟩$
23 18 22 eqtrd ${⊢}\left({\phi }\wedge {i}=1\right)\to ⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)=⟨“{C}{D}”⟩$
24 23 fveq2d ${⊢}\left({\phi }\wedge {i}=1\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=\left|⟨“{C}{D}”⟩\right|$
25 s2len ${⊢}\left|⟨“{C}{D}”⟩\right|=2$
26 24 25 syl6eq ${⊢}\left({\phi }\wedge {i}=1\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$
27 26 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\wedge {i}=1\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$
28 fzo0to2pr ${⊢}\left(0..^2\right)=\left\{0,1\right\}$
29 28 eleq2i ${⊢}{i}\in \left(0..^2\right)↔{i}\in \left\{0,1\right\}$
30 vex ${⊢}{i}\in \mathrm{V}$
31 30 elpr ${⊢}{i}\in \left\{0,1\right\}↔\left({i}=0\vee {i}=1\right)$
32 29 31 bitri ${⊢}{i}\in \left(0..^2\right)↔\left({i}=0\vee {i}=1\right)$
33 32 biimpi ${⊢}{i}\in \left(0..^2\right)\to \left({i}=0\vee {i}=1\right)$
34 33 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\to \left({i}=0\vee {i}=1\right)$
35 16 27 34 mpjaodan ${⊢}\left({\phi }\wedge {i}\in \left(0..^2\right)\right)\to \left|⟨“⟨“{A}{B}”⟩⟨“{C}{D}”⟩”⟩\left({i}\right)\right|=2$