madulid

Description: Multiplying the adjunct of a matrix with the matrix results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018)

	Ref	Expression
Hypotheses	madurid.a	$⊢ A = N Mat R$
	madurid.b	$⊢ B = {Base}_{A}$
	madurid.j	$⊢ J = N maAdju R$
	madurid.d	$⊢ D = N maDet R$
	madurid.i	$⊢ \underset{˙}{1} = 1_{A}$
	madurid.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	madurid.s	$⊢ \underset{˙}{∙} = \cdot_{A}$
Assertion	madulid	$⊢ (M \in B \land R \in CRing) \to J (M) \underset{˙}{\cdot} M = D (M) \underset{˙}{∙} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		madurid.a	$⊢ A = N Mat R$
2		madurid.b	$⊢ B = {Base}_{A}$
3		madurid.j	$⊢ J = N maAdju R$
4		madurid.d	$⊢ D = N maDet R$
5		madurid.i	$⊢ \underset{˙}{1} = 1_{A}$
6		madurid.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
7		madurid.s	$⊢ \underset{˙}{∙} = \cdot_{A}$
8		simpr	$⊢ (M \in B \land R \in CRing) \to R \in CRing$
9	1 3 2	maduf	$⊢ R \in CRing \to J : B ⟶ B$
10	9	ffvelrnda	$⊢ (R \in CRing \land M \in B) \to J (M) \in B$
11	10	ancoms	$⊢ (M \in B \land R \in CRing) \to J (M) \in B$
12		simpl	$⊢ (M \in B \land R \in CRing) \to M \in B$
13	1 2 6	mattposm	$⊢ (R \in CRing \land J (M) \in B \land M \in B) \to tpos (J (M) \underset{˙}{\cdot} M) = tpos M \underset{˙}{\cdot} tpos J (M)$
14	8 11 12 13	syl3anc	$⊢ (M \in B \land R \in CRing) \to tpos (J (M) \underset{˙}{\cdot} M) = tpos M \underset{˙}{\cdot} tpos J (M)$
15	1 3 2	madutpos	$⊢ (R \in CRing \land M \in B) \to J (tpos M) = tpos J (M)$
16	15	ancoms	$⊢ (M \in B \land R \in CRing) \to J (tpos M) = tpos J (M)$
17	16	oveq2d	$⊢ (M \in B \land R \in CRing) \to tpos M \underset{˙}{\cdot} J (tpos M) = tpos M \underset{˙}{\cdot} tpos J (M)$
18	1 2	mattposcl	$⊢ M \in B \to tpos M \in B$
19	1 2 3 4 5 6 7	madurid	$⊢ (tpos M \in B \land R \in CRing) \to tpos M \underset{˙}{\cdot} J (tpos M) = D (tpos M) \underset{˙}{∙} \underset{˙}{1}$
20	18 19	sylan	$⊢ (M \in B \land R \in CRing) \to tpos M \underset{˙}{\cdot} J (tpos M) = D (tpos M) \underset{˙}{∙} \underset{˙}{1}$
21	14 17 20	3eqtr2d	$⊢ (M \in B \land R \in CRing) \to tpos (J (M) \underset{˙}{\cdot} M) = D (tpos M) \underset{˙}{∙} \underset{˙}{1}$
22	21	tposeqd	$⊢ (M \in B \land R \in CRing) \to tpos tpos (J (M) \underset{˙}{\cdot} M) = tpos (D (tpos M) \underset{˙}{∙} \underset{˙}{1})$
23	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
24	23	simpld	$⊢ M \in B \to N \in Fin$
25		crngring	$⊢ R \in CRing \to R \in Ring$
26	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
27	24 25 26	syl2an	$⊢ (M \in B \land R \in CRing) \to A \in Ring$
28	2 6	ringcl	$⊢ (A \in Ring \land J (M) \in B \land M \in B) \to J (M) \underset{˙}{\cdot} M \in B$
29	27 11 12 28	syl3anc	$⊢ (M \in B \land R \in CRing) \to J (M) \underset{˙}{\cdot} M \in B$
30	1 2	mattpostpos	$⊢ J (M) \underset{˙}{\cdot} M \in B \to tpos tpos (J (M) \underset{˙}{\cdot} M) = J (M) \underset{˙}{\cdot} M$
31	29 30	syl	$⊢ (M \in B \land R \in CRing) \to tpos tpos (J (M) \underset{˙}{\cdot} M) = J (M) \underset{˙}{\cdot} M$
32		eqid	$⊢ {Base}_{R} = {Base}_{R}$
33	4 1 2 32	mdetf	$⊢ R \in CRing \to D : B ⟶ {Base}_{R}$
34	33	adantl	$⊢ (M \in B \land R \in CRing) \to D : B ⟶ {Base}_{R}$
35	18	adantr	$⊢ (M \in B \land R \in CRing) \to tpos M \in B$
36	34 35	ffvelrnd	$⊢ (M \in B \land R \in CRing) \to D (tpos M) \in {Base}_{R}$
37	2 5	ringidcl	$⊢ A \in Ring \to \underset{˙}{1} \in B$
38	27 37	syl	$⊢ (M \in B \land R \in CRing) \to \underset{˙}{1} \in B$
39	1 2 32 7	mattposvs	$⊢ (D (tpos M) \in {Base}_{R} \land \underset{˙}{1} \in B) \to tpos (D (tpos M) \underset{˙}{∙} \underset{˙}{1}) = D (tpos M) \underset{˙}{∙} tpos \underset{˙}{1}$
40	36 38 39	syl2anc	$⊢ (M \in B \land R \in CRing) \to tpos (D (tpos M) \underset{˙}{∙} \underset{˙}{1}) = D (tpos M) \underset{˙}{∙} tpos \underset{˙}{1}$
41	4 1 2	mdettpos	$⊢ (R \in CRing \land M \in B) \to D (tpos M) = D (M)$
42	41	ancoms	$⊢ (M \in B \land R \in CRing) \to D (tpos M) = D (M)$
43	1 5	mattpos1	$⊢ (N \in Fin \land R \in Ring) \to tpos \underset{˙}{1} = \underset{˙}{1}$
44	24 25 43	syl2an	$⊢ (M \in B \land R \in CRing) \to tpos \underset{˙}{1} = \underset{˙}{1}$
45	42 44	oveq12d	$⊢ (M \in B \land R \in CRing) \to D (tpos M) \underset{˙}{∙} tpos \underset{˙}{1} = D (M) \underset{˙}{∙} \underset{˙}{1}$
46	40 45	eqtrd	$⊢ (M \in B \land R \in CRing) \to tpos (D (tpos M) \underset{˙}{∙} \underset{˙}{1}) = D (M) \underset{˙}{∙} \underset{˙}{1}$
47	22 31 46	3eqtr3d	$⊢ (M \in B \land R \in CRing) \to J (M) \underset{˙}{\cdot} M = D (M) \underset{˙}{∙} \underset{˙}{1}$

Metamath Proof Explorer

Theorem madulid

Proof