Metamath Proof Explorer


Theorem madurid

Description: Multiplying a matrix with its adjunct 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, 16-Jul-2018)

Ref Expression
Hypotheses madurid.a A = N Mat R
madurid.b B = Base A
madurid.j J = N maAdju R
madurid.d D = N maDet R
madurid.i 1 ˙ = 1 A
madurid.t · ˙ = A
madurid.s ˙ = A
Assertion madurid M B R CRing M · ˙ J M = D M ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 madurid.a A = N Mat R
2 madurid.b B = Base A
3 madurid.j J = N maAdju R
4 madurid.d D = N maDet R
5 madurid.i 1 ˙ = 1 A
6 madurid.t · ˙ = A
7 madurid.s ˙ = A
8 eqid R maMul N N N = R maMul N N N
9 eqid Base R = Base R
10 eqid R = R
11 simpr M B R CRing R CRing
12 1 2 matrcl M B N Fin R V
13 12 simpld M B N Fin
14 13 adantr M B R CRing N Fin
15 1 9 2 matbas2i M B M Base R N × N
16 15 adantr M B R CRing M Base R N × N
17 1 3 2 maduf R CRing J : B B
18 17 adantl M B R CRing J : B B
19 simpl M B R CRing M B
20 18 19 ffvelrnd M B R CRing J M B
21 1 9 2 matbas2i J M B J M Base R N × N
22 20 21 syl M B R CRing J M Base R N × N
23 8 9 10 11 14 14 14 16 22 mamuval M B R CRing M R maMul N N N J M = a N , b N R c N a M c R c J M b
24 1 8 matmulr N Fin R CRing R maMul N N N = A
25 13 24 sylan M B R CRing R maMul N N N = A
26 25 6 syl6eqr M B R CRing R maMul N N N = · ˙
27 26 oveqd M B R CRing M R maMul N N N J M = M · ˙ J M
28 simp1l M B R CRing a N b N M B
29 simp1r M B R CRing a N b N R CRing
30 elmapi M Base R N × N M : N × N Base R
31 16 30 syl M B R CRing M : N × N Base R
32 31 3ad2ant1 M B R CRing a N b N M : N × N Base R
33 32 adantr M B R CRing a N b N c N M : N × N Base R
34 simpl2 M B R CRing a N b N c N a N
35 simpr M B R CRing a N b N c N c N
36 33 34 35 fovrnd M B R CRing a N b N c N a M c Base R
37 simp3 M B R CRing a N b N b N
38 1 3 2 4 10 9 28 29 36 37 madugsum M B R CRing a N b N R c N a M c R c J M b = D d N , c N if d = b a M c d M c
39 iftrue a = b if a = b D M 0 R = D M
40 39 adantl M B R CRing a = b if a = b D M 0 R = D M
41 31 ffnd M B R CRing M Fn N × N
42 fnov M Fn N × N M = d N , c N d M c
43 41 42 sylib M B R CRing M = d N , c N d M c
44 43 adantr M B R CRing a = b M = d N , c N d M c
45 equtr2 a = b d = b a = d
46 45 oveq1d a = b d = b a M c = d M c
47 46 ifeq1da a = b if d = b a M c d M c = if d = b d M c d M c
48 ifid if d = b d M c d M c = d M c
49 47 48 syl6eq a = b if d = b a M c d M c = d M c
50 49 adantl M B R CRing a = b if d = b a M c d M c = d M c
51 50 mpoeq3dv M B R CRing a = b d N , c N if d = b a M c d M c = d N , c N d M c
52 44 51 eqtr4d M B R CRing a = b M = d N , c N if d = b a M c d M c
53 52 fveq2d M B R CRing a = b D M = D d N , c N if d = b a M c d M c
54 40 53 eqtr2d M B R CRing a = b D d N , c N if d = b a M c d M c = if a = b D M 0 R
55 54 3ad2antl1 M B R CRing a N b N a = b D d N , c N if d = b a M c d M c = if a = b D M 0 R
56 eqid 0 R = 0 R
57 simpl1r M B R CRing a N b N ¬ a = b R CRing
58 14 3ad2ant1 M B R CRing a N b N N Fin
59 58 adantr M B R CRing a N b N ¬ a = b N Fin
60 32 ad2antrr M B R CRing a N b N ¬ a = b c N M : N × N Base R
61 simpll2 M B R CRing a N b N ¬ a = b c N a N
62 simpr M B R CRing a N b N ¬ a = b c N c N
63 60 61 62 fovrnd M B R CRing a N b N ¬ a = b c N a M c Base R
64 32 adantr M B R CRing a N b N ¬ a = b M : N × N Base R
65 64 fovrnda M B R CRing a N b N ¬ a = b d N c N d M c Base R
66 65 3impb M B R CRing a N b N ¬ a = b d N c N d M c Base R
67 simpl3 M B R CRing a N b N ¬ a = b b N
68 simpl2 M B R CRing a N b N ¬ a = b a N
69 neqne ¬ a = b a b
70 69 necomd ¬ a = b b a
71 70 adantl M B R CRing a N b N ¬ a = b b a
72 4 9 56 57 59 63 66 67 68 71 mdetralt2 M B R CRing a N b N ¬ a = b D d N , c N if d = b a M c if d = a a M c d M c = 0 R
73 ifid if d = a d M c d M c = d M c
74 oveq1 d = a d M c = a M c
75 74 adantl M B R CRing a N b N ¬ a = b d = a d M c = a M c
76 75 ifeq1da M B R CRing a N b N ¬ a = b if d = a d M c d M c = if d = a a M c d M c
77 73 76 syl5eqr M B R CRing a N b N ¬ a = b d M c = if d = a a M c d M c
78 77 ifeq2d M B R CRing a N b N ¬ a = b if d = b a M c d M c = if d = b a M c if d = a a M c d M c
79 78 mpoeq3dv M B R CRing a N b N ¬ a = b d N , c N if d = b a M c d M c = d N , c N if d = b a M c if d = a a M c d M c
80 79 fveq2d M B R CRing a N b N ¬ a = b D d N , c N if d = b a M c d M c = D d N , c N if d = b a M c if d = a a M c d M c
81 iffalse ¬ a = b if a = b D M 0 R = 0 R
82 81 adantl M B R CRing a N b N ¬ a = b if a = b D M 0 R = 0 R
83 72 80 82 3eqtr4d M B R CRing a N b N ¬ a = b D d N , c N if d = b a M c d M c = if a = b D M 0 R
84 55 83 pm2.61dan M B R CRing a N b N D d N , c N if d = b a M c d M c = if a = b D M 0 R
85 38 84 eqtrd M B R CRing a N b N R c N a M c R c J M b = if a = b D M 0 R
86 85 mpoeq3dva M B R CRing a N , b N R c N a M c R c J M b = a N , b N if a = b D M 0 R
87 5 oveq2i D M ˙ 1 ˙ = D M ˙ 1 A
88 crngring R CRing R Ring
89 88 adantl M B R CRing R Ring
90 4 1 2 9 mdetf R CRing D : B Base R
91 90 adantl M B R CRing D : B Base R
92 91 19 ffvelrnd M B R CRing D M Base R
93 1 9 7 56 matsc N Fin R Ring D M Base R D M ˙ 1 A = a N , b N if a = b D M 0 R
94 14 89 92 93 syl3anc M B R CRing D M ˙ 1 A = a N , b N if a = b D M 0 R
95 87 94 syl5eq M B R CRing D M ˙ 1 ˙ = a N , b N if a = b D M 0 R
96 86 95 eqtr4d M B R CRing a N , b N R c N a M c R c J M b = D M ˙ 1 ˙
97 23 27 96 3eqtr3d M B R CRing M · ˙ J M = D M ˙ 1 ˙