cpmadurid

Description: The right-hand fundamental relation of the adjugate (see madurid ) applied to the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019)

	Ref	Expression
Hypotheses	cpmadurid.a	$⊢ A = N Mat R$
	cpmadurid.b	$⊢ B = {Base}_{A}$
	cpmadurid.c	$⊢ C = N CharPlyMat R$
	cpmadurid.p	$⊢ P = {Poly}_{1} (R)$
	cpmadurid.y	$⊢ Y = N Mat P$
	cpmadurid.x	$⊢ X = {var}_{1} (R)$
	cpmadurid.t	$⊢ T = N matToPolyMat R$
	cpmadurid.s	$⊢ \underset{˙}{-} = -_{Y}$
	cpmadurid.m1	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmadurid.1	$⊢ \underset{˙}{1} = 1_{Y}$
	cpmadurid.i	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
	cpmadurid.j	$⊢ J = N maAdju P$
	cpmadurid.m2	$⊢ \underset{˙}{\times} = \cdot_{Y}$
Assertion	cpmadurid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \underset{˙}{\times} J (I) = C (M) \underset{˙}{\cdot} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		cpmadurid.a	$⊢ A = N Mat R$
2		cpmadurid.b	$⊢ B = {Base}_{A}$
3		cpmadurid.c	$⊢ C = N CharPlyMat R$
4		cpmadurid.p	$⊢ P = {Poly}_{1} (R)$
5		cpmadurid.y	$⊢ Y = N Mat P$
6		cpmadurid.x	$⊢ X = {var}_{1} (R)$
7		cpmadurid.t	$⊢ T = N matToPolyMat R$
8		cpmadurid.s	$⊢ \underset{˙}{-} = -_{Y}$
9		cpmadurid.m1	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
10		cpmadurid.1	$⊢ \underset{˙}{1} = 1_{Y}$
11		cpmadurid.i	$⊢ I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
12		cpmadurid.j	$⊢ J = N maAdju P$
13		cpmadurid.m2	$⊢ \underset{˙}{\times} = \cdot_{Y}$
14		crngring	$⊢ R \in CRing \to R \in Ring$
15	1 2 4 5 6 7 8 9 10 11	chmatcl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to I \in {Base}_{Y}$
16	14 15	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \in {Base}_{Y}$
17	4	ply1crng	$⊢ R \in CRing \to P \in CRing$
18	17	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in CRing$
19		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
20		eqid	$⊢ N maDet P = N maDet P$
21	5 19 12 20 10 13 9	madurid	$⊢ (I \in {Base}_{Y} \land P \in CRing) \to I \underset{˙}{\times} J (I) = (N maDet P) (I) \underset{˙}{\cdot} \underset{˙}{1}$
22	16 18 21	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \underset{˙}{\times} J (I) = (N maDet P) (I) \underset{˙}{\cdot} \underset{˙}{1}$
23	3 1 2 4 5 20 8 6 9 7 10	chpmatval	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) = (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M))$
24	11	a1i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
25	24	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M) = I$
26	25	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N maDet P) ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) = (N maDet P) (I)$
27	23 26	eqtr2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N maDet P) (I) = C (M)$
28	27	oveq1d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N maDet P) (I) \underset{˙}{\cdot} \underset{˙}{1} = C (M) \underset{˙}{\cdot} \underset{˙}{1}$
29	22 28	eqtrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I \underset{˙}{\times} J (I) = C (M) \underset{˙}{\cdot} \underset{˙}{1}$

Metamath Proof Explorer

Theorem cpmadurid

Proof