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(⟨“⟨“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	lmat22e21	$$⊢\phi \to 2M1=C$$

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		0nn0	$$⊢0\in {\mathbb{N}}_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	$$⊢⟨“CD”⟩\in \mathrm{Word}\mathrm{V}$$
22		s2fv1	$$⊢⟨“CD”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1\right)=⟨“CD”⟩$$
23	21 22	ax-mp	$$⊢⟨“⟨“AB”⟩⟨“CD”⟩”⟩\left(1\right)=⟨“CD”⟩$$
24		s2fv0	$$⊢C\in V\to ⟨“CD”⟩\left(0\right)=C$$
25	4 24	syl	$$⊢\phi \to ⟨“CD”⟩\left(0\right)=C$$
26	1 7 10 12 13 14 15 17 18 19 20 23 25	lmatfvlem	$$⊢\phi \to 2M1=C$$