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 = ( Poly1 ` R )
	cpmadurid.y	\|- Y = ( N Mat P )
	cpmadurid.x	\|- X = ( var1 ` R )
	cpmadurid.t	\|- T = ( N matToPolyMat R )
	cpmadurid.s	\|- .- = ( -g ` Y )
	cpmadurid.m1	\|- .x. = ( .s ` Y )
	cpmadurid.1	\|- .1. = ( 1r ` Y )
	cpmadurid.i	\|- I = ( ( X .x. .1. ) .- ( T ` M ) )
	cpmadurid.j	\|- J = ( N maAdju P )
	cpmadurid.m2	\|- .X. = ( .r ` Y )
Assertion	cpmadurid	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I .X. ( J ` I ) ) = ( ( C ` M ) .x. .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 = ( Poly1 ` R )
5		cpmadurid.y	\|- Y = ( N Mat P )
6		cpmadurid.x	\|- X = ( var1 ` R )
7		cpmadurid.t	\|- T = ( N matToPolyMat R )
8		cpmadurid.s	\|- .- = ( -g ` Y )
9		cpmadurid.m1	\|- .x. = ( .s ` Y )
10		cpmadurid.1	\|- .1. = ( 1r ` Y )
11		cpmadurid.i	\|- I = ( ( X .x. .1. ) .- ( T ` M ) )
12		cpmadurid.j	\|- J = ( N maAdju P )
13		cpmadurid.m2	\|- .X. = ( .r ` Y )
14		crngring	\|- ( R e. CRing -> R e. Ring )
15	1 2 4 5 6 7 8 9 10 11	chmatcl	\|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> I e. ( Base ` Y ) )
16	14 15	syl3an2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> I e. ( Base ` Y ) )
17	4	ply1crng	\|- ( R e. CRing -> P e. CRing )
18	17	3ad2ant2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. 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 e. ( Base ` Y ) /\ P e. CRing ) -> ( I .X. ( J ` I ) ) = ( ( ( N maDet P ) ` I ) .x. .1. ) )
22	16 18 21	syl2anc	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I .X. ( J ` I ) ) = ( ( ( N maDet P ) ` I ) .x. .1. ) )
23	3 1 2 4 5 20 8 6 9 7 10	chpmatval	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
24	11	a1i	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> I = ( ( X .x. .1. ) .- ( T ` M ) ) )
25	24	eqcomd	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) = I )
26	25	fveq2d	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) = ( ( N maDet P ) ` I ) )
27	23 26	eqtr2d	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( N maDet P ) ` I ) = ( C ` M ) )
28	27	oveq1d	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( N maDet P ) ` I ) .x. .1. ) = ( ( C ` M ) .x. .1. ) )
29	22 28	eqtrd	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I .X. ( J ` I ) ) = ( ( C ` M ) .x. .1. ) )

Metamath Proof Explorer

Theorem cpmadurid

Proof