Theorem 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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmadurid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmadurid.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cpmadurid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmadurid.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmadurid.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmadurid.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmadurid.s	⊢ − = ( -g ‘ 𝑌 )
	cpmadurid.m1	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmadurid.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmadurid.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
	cpmadurid.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
	cpmadurid.m2	⊢ × = ( .r ‘ 𝑌 )
Assertion	cpmadurid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐶 ‘ 𝑀 ) · 1 ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadurid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmadurid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmadurid.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
4		cpmadurid.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		cpmadurid.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
6		cpmadurid.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		cpmadurid.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8		cpmadurid.s	⊢ − = ( -g ‘ 𝑌 )
9		cpmadurid.m1	⊢ · = ( ·𝑠 ‘ 𝑌 )
10		cpmadurid.1	⊢ 1 = ( 1r ‘ 𝑌 )
11		cpmadurid.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
12		cpmadurid.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
13		cpmadurid.m2	⊢ × = ( .r ‘ 𝑌 )
14		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
15	1 2 4 5 6 7 8 9 10 11	chmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐼 ∈ ( Base ‘ 𝑌 ) )
16	14 15	syl3an2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐼 ∈ ( Base ‘ 𝑌 ) )
17	4	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
18	17	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CRing )
19		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
20		eqid	⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
21	5 19 12 20 10 13 9	madurid	⊢ ( ( 𝐼 ∈ ( Base ‘ 𝑌 ) ∧ 𝑃 ∈ CRing ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ 𝐼 ) · 1 ) )
22	16 18 21	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( ( 𝑁 maDet 𝑃 ) ‘ 𝐼 ) · 1 ) )
23	3 1 2 4 5 20 8 6 9 7 10	chpmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) )
24	11	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) )
25	24	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) = 𝐼 )
26	25	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ) = ( ( 𝑁 maDet 𝑃 ) ‘ 𝐼 ) )
27	23 26	eqtr2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ 𝐼 ) = ( 𝐶 ‘ 𝑀 ) )
28	27	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( ( 𝑁 maDet 𝑃 ) ‘ 𝐼 ) · 1 ) = ( ( 𝐶 ‘ 𝑀 ) · 1 ) )
29	22 28	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐶 ‘ 𝑀 ) · 1 ) )