Theorem lmat22det

Description: The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-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$$
	lmat22det.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	lmat22det.s	$$⊢\underset{\dot{}}{-}={-}_R$$
	lmat22det.v	$$⊢V={\mathrm{Base}}_R$$
	lmat22det.j	$$⊢J=\left(1\dots 2\right)\mathrm{maDet}R$$
	lmat22det.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	lmat22det	$$⊢\phi \to J\left(M\right)=\left(A\underset{\dot{}}{·}D\right)\underset{\dot{}}{-}\left(C\underset{\dot{}}{·}B\right)$$

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		lmat22det.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		lmat22det.s	$$⊢\underset{\dot{}}{-}={-}_R$$
8		lmat22det.v	$$⊢V={\mathrm{Base}}_R$$
9		lmat22det.j	$$⊢J=\left(1\dots 2\right)\mathrm{maDet}R$$
10		lmat22det.r	$$⊢\phi \to R\in \mathrm{Ring}$$
11		2nn	$$⊢2\in \mathbb{N}$$
12	11	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
13	2 3	s2cld	$$⊢\phi \to ⟨“AB”⟩\in \mathrm{Word}V$$
14	4 5	s2cld	$$⊢\phi \to ⟨“CD”⟩\in \mathrm{Word}V$$
15	13 14	s2cld	$$⊢\phi \to ⟨“⟨“AB”⟩⟨“CD”⟩”⟩\in \mathrm{Word}\mathrm{Word}V$$
16		s2len	$$⊢\left|⟨“⟨“AB”⟩⟨“CD”⟩”⟩\right|=2$$
17	16	a1i	$$⊢\phi \to \left|⟨“⟨“AB”⟩⟨“CD”⟩”⟩\right|=2$$
18	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$$
19		eqid	$$⊢\left(1\dots 2\right)\mathrm{Mat}R=\left(1\dots 2\right)\mathrm{Mat}R$$
20		eqid	$$⊢{\mathrm{Base}}_{\left(\left(1\dots 2\right)\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(\left(1\dots 2\right)\mathrm{Mat}R\right)}$$
21	1 12 15 17 18 8 19 20 10	lmatcl	$$⊢\phi \to M\in {\mathrm{Base}}_{\left(\left(1\dots 2\right)\mathrm{Mat}R\right)}$$
22		2z	$$⊢2\in \mathbb{Z}$$
23		fzval3	$$⊢2\in \mathbb{Z}\to \left(1\dots 2\right)=\left(1..^2+1\right)$$
24	22 23	ax-mp	$$⊢\left(1\dots 2\right)=\left(1..^2+1\right)$$
25		2p1e3	$$⊢2+1=3$$
26	25	oveq2i	$$⊢\left(1..^2+1\right)=\left(1..^3\right)$$
27		fzo13pr	$$⊢\left(1..^3\right)=\left\{1,2\right\}$$
28	24 26 27	3eqtri	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
29	28 9 19 20 7 6	m2detleib	$$⊢\left(R\in \mathrm{Ring}\wedge M\in {\mathrm{Base}}_{\left(\left(1\dots 2\right)\mathrm{Mat}R\right)}\right)\to J\left(M\right)=\left(\left(1M1\right)\underset{\dot{}}{·}\left(2M2\right)\right)\underset{\dot{}}{-}\left(\left(2M1\right)\underset{\dot{}}{·}\left(1M2\right)\right)$$
30	10 21 29	syl2anc	$$⊢\phi \to J\left(M\right)=\left(\left(1M1\right)\underset{\dot{}}{·}\left(2M2\right)\right)\underset{\dot{}}{-}\left(\left(2M1\right)\underset{\dot{}}{·}\left(1M2\right)\right)$$
31	1 2 3 4 5	lmat22e11	$$⊢\phi \to 1M1=A$$
32	1 2 3 4 5	lmat22e22	$$⊢\phi \to 2M2=D$$
33	31 32	oveq12d	$$⊢\phi \to \left(1M1\right)\underset{\dot{}}{·}\left(2M2\right)=A\underset{\dot{}}{·}D$$
34	1 2 3 4 5	lmat22e21	$$⊢\phi \to 2M1=C$$
35	1 2 3 4 5	lmat22e12	$$⊢\phi \to 1M2=B$$
36	34 35	oveq12d	$$⊢\phi \to \left(2M1\right)\underset{\dot{}}{·}\left(1M2\right)=C\underset{\dot{}}{·}B$$
37	33 36	oveq12d	$$⊢\phi \to \left(\left(1M1\right)\underset{\dot{}}{·}\left(2M2\right)\right)\underset{\dot{}}{-}\left(\left(2M1\right)\underset{\dot{}}{·}\left(1M2\right)\right)=\left(A\underset{\dot{}}{·}D\right)\underset{\dot{}}{-}\left(C\underset{\dot{}}{·}B\right)$$
38	30 37	eqtrd	$$⊢\phi \to J\left(M\right)=\left(A\underset{\dot{}}{·}D\right)\underset{\dot{}}{-}\left(C\underset{\dot{}}{·}B\right)$$