This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 = ( 1r ‘ 𝐴 )
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 = ( 1r ‘ 𝐴 )
6 madurid.t ⊢ · = ( .r ‘ 𝐴 )
7 madurid.s ⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
8 simpr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
9 1 3 2 maduf ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
10 9 ffvelcdmda ⊢ ( ( 𝑅 ∈ 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 ffvelcdmd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ 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 ) )