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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	madurid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madurid.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
	madurid.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	madurid.i	⊢ 1 = ( 1_r ‘ 𝐴 )
	madurid.t	⊢ · = ( ._r ‘ 𝐴 )
	madurid.s	⊢ ∙ = ( ·_𝑠 ‘ 𝐴 )
Assertion	madulid	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		madurid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		madurid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		madurid.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
4		madurid.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5		madurid.i	⊢ 1 = ( 1_r ‘ 𝐴 )
6		madurid.t	⊢ · = ( ._r ‘ 𝐴 )
7		madurid.s	⊢ ∙ = ( ·_𝑠 ‘ 𝐴 )
8		simpr	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
9	1 3 2	maduf	⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
10	9	ffvelrnda	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
11	10	ancoms	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
12		simpl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ 𝐵 )
13	1 2 6	mattposm	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 ∧ 𝑀 ∈ 𝐵 ) → tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( tpos 𝑀 · tpos ( 𝐽 ‘ 𝑀 ) ) )
14	8 11 12 13	syl3anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( tpos 𝑀 · tpos ( 𝐽 ‘ 𝑀 ) ) )
15	1 3 2	madutpos	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ tpos 𝑀 ) = tpos ( 𝐽 ‘ 𝑀 ) )
16	15	ancoms	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐽 ‘ tpos 𝑀 ) = tpos ( 𝐽 ‘ 𝑀 ) )
17	16	oveq2d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( tpos 𝑀 · ( 𝐽 ‘ tpos 𝑀 ) ) = ( tpos 𝑀 · tpos ( 𝐽 ‘ 𝑀 ) ) )
18	1 2	mattposcl	⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )
19	1 2 3 4 5 6 7	madurid	⊢ ( ( tpos 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( tpos 𝑀 · ( 𝐽 ‘ tpos 𝑀 ) ) = ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) )
20	18 19	sylan	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( tpos 𝑀 · ( 𝐽 ‘ tpos 𝑀 ) ) = ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) )
21	14 17 20	3eqtr2d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) )
22	21	tposeqd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = tpos ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) )
23	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
24	23	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
25		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
27	24 25 26	syl2an	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
28	2 6	ringcl	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) ∈ 𝐵 )
29	27 11 12 28	syl3anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) ∈ 𝐵 )
30	1 2	mattpostpos	⊢ ( ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) ∈ 𝐵 → tpos tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) )
31	29 30	syl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos tpos ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) )
32		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33	4 1 2 32	mdetf	⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
34	33	adantl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
35	18	adantr	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos 𝑀 ∈ 𝐵 )
36	34 35	ffvelrnd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐷 ‘ tpos 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
37	2 5	ringidcl	⊢ ( 𝐴 ∈ Ring → 1 ∈ 𝐵 )
38	27 37	syl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 1 ∈ 𝐵 )
39	1 2 32 7	mattposvs	⊢ ( ( ( 𝐷 ‘ tpos 𝑀 ) ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ 𝐵 ) → tpos ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) = ( ( 𝐷 ‘ tpos 𝑀 ) ∙ tpos 1 ) )
40	36 38 39	syl2anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) = ( ( 𝐷 ‘ tpos 𝑀 ) ∙ tpos 1 ) )
41	4 1 2	mdettpos	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ tpos 𝑀 ) = ( 𝐷 ‘ 𝑀 ) )
42	41	ancoms	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐷 ‘ tpos 𝑀 ) = ( 𝐷 ‘ 𝑀 ) )
43	1 5	mattpos1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → tpos 1 = 1 )
44	24 25 43	syl2an	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos 1 = 1 )
45	42 44	oveq12d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐷 ‘ tpos 𝑀 ) ∙ tpos 1 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )
46	40 45	eqtrd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → tpos ( ( 𝐷 ‘ tpos 𝑀 ) ∙ 1 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )
47	22 31 46	3eqtr3d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐽 ‘ 𝑀 ) · 𝑀 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )

Metamath Proof Explorer

Theorem madulid

Proof