Theorem lmat22e11

Description: Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Hypotheses	lmat22.m	$$⊢M=\mathrm{litMat}\left(⟨“⟨“AB”⟩⟨“CD”⟩”⟩\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	lmat22e11	$$⊢\phi \to 1M1=A$$

Proof

Step	Hyp	Ref	Expression
1		lmat22.m	$$⊢M=\mathrm{litMat}\left(⟨“⟨“AB”⟩⟨“CD”⟩”⟩\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 \mathbb{N}$$
7	6	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
8	2 3	s2cld	$$⊢\phi \to ⟨“AB”⟩\in \mathrm{Word}V$$
9	4 5	s2cld	$$⊢\phi \to ⟨“CD”⟩\in \mathrm{Word}V$$
10	8 9	s2cld	$$⊢\phi \to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\in \mathrm{Word}\mathrm{Word}V$$
11		s2len	$$⊢\left|⟨“⟨“AB”⟩⟨“CD”⟩”⟩\right|=2$$
12	11	a1i	$$⊢\phi \to \left|⟨“⟨“AB”⟩⟨“CD”⟩”⟩\right|=2$$
13	1 2 3 4 5	lmat22lem	$$⊢\left(\phi \wedge i\in \left(0..^2\right)\right)\to \left|⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(i\right)\right|=2$$
14		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
15		eluzfz1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots 2\right)$$
16	14 15	ax-mp	$$⊢1\in \left(1\dots 2\right)$$
17	16	a1i	$$⊢\phi \to 1\in \left(1\dots 2\right)$$
18	1 7 10 12 13 17 17	lmatfval	$$⊢\phi \to 1M1=⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1-1\right)\left(1-1\right)$$
19		1m1e0	$$⊢1-1=0$$
20	19	fveq2i	$$⊢⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1-1\right)=⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(0\right)$$
21		s2fv0	$$⊢⟨“AB”⟩\in \mathrm{Word}V\to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(0\right)=⟨“AB”⟩$$
22	8 21	syl	$$⊢\phi \to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(0\right)=⟨“AB”⟩$$
23	20 22	syl5eq	$$⊢\phi \to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1-1\right)=⟨“AB”⟩$$
24	19	a1i	$$⊢\phi \to 1-1=0$$
25	23 24	fveq12d	$$⊢\phi \to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1-1\right)\left(1-1\right)=⟨“AB”⟩\left(0\right)$$
26		s2fv0	$$⊢A\in V\to ⟨“AB”⟩\left(0\right)=A$$
27	2 26	syl	$$⊢\phi \to ⟨“AB”⟩\left(0\right)=A$$
28	18 25 27	3eqtrd	$$⊢\phi \to 1M1=A$$