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(⟨“⟨“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	lmat22e22	$$⊢\phi \to 2M2=D$$

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