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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
madurid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madurid.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
madurid.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
madurid.i ⊢ 1 = ( 1r ‘ 𝐴 )
madurid.t ⊢ · = ( .r ‘ 𝐴 )
madurid.s ⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
Assertion madurid ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ 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 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 simpr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
12 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
13 12 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
14 13 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑁 ∈ Fin )
15 1 9 2 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
16 15 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17 1 3 2 maduf ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
18 17 adantl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝐽 : 𝐵 ⟶ 𝐵 )
19 simpl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ 𝐵 )
20 18 19 ffvelcdmd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
21 1 9 2 matbas2i ⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 → ( 𝐽 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
22 20 21 syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐽 ‘ 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
23 8 9 10 11 14 14 14 16 22 mamuval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑀 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐽 ‘ 𝑀 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑎 𝑀 𝑐 ) ( .r ‘ 𝑅 ) ( 𝑐 ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) ) ) ) )
24 1 8 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
25 13 24 sylan ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
26 25 6 eqtr4di ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = · )
27 26 oveqd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑀 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝐽 ‘ 𝑀 ) ) = ( 𝑀 · ( 𝐽 ‘ 𝑀 ) ) )
28 simp1l ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
29 simp1r ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ CRing )
30 elmapi ⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
31 16 30 syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
32 31 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
33 32 adantr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
34 simpl2 ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
35 simpr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
36 33 34 35 fovcdmd ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝑎 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
37 simp3 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
38 1 3 2 4 10 9 28 29 36 37 madugsum ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑎 𝑀 𝑐 ) ( .r ‘ 𝑅 ) ( 𝑐 ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
39 iftrue ⊢ ( 𝑎 = 𝑏 → if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ 𝑀 ) )
40 39 adantl ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ 𝑀 ) )
41 31 ffnd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 Fn ( 𝑁 × 𝑁 ) )
42 fnov ⊢ ( 𝑀 Fn ( 𝑁 × 𝑁 ) ↔ 𝑀 = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ ( 𝑑 𝑀 𝑐 ) ) )
43 41 42 sylib ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑀 = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ ( 𝑑 𝑀 𝑐 ) ) )
44 43 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → 𝑀 = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ ( 𝑑 𝑀 𝑐 ) ) )
45 equtr2 ⊢ ( ( 𝑎 = 𝑏 ∧ 𝑑 = 𝑏 ) → 𝑎 = 𝑑 )
46 45 oveq1d ⊢ ( ( 𝑎 = 𝑏 ∧ 𝑑 = 𝑏 ) → ( 𝑎 𝑀 𝑐 ) = ( 𝑑 𝑀 𝑐 ) )
47 46 ifeq1da ⊢ ( 𝑎 = 𝑏 → if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = if ( 𝑑 = 𝑏 , ( 𝑑 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) )
48 ifid ⊢ if ( 𝑑 = 𝑏 , ( 𝑑 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = ( 𝑑 𝑀 𝑐 )
49 47 48 eqtrdi ⊢ ( 𝑎 = 𝑏 → if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = ( 𝑑 𝑀 𝑐 ) )
50 49 adantl ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = ( 𝑑 𝑀 𝑐 ) )
51 50 mpoeq3dv ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ ( 𝑑 𝑀 𝑐 ) ) )
52 44 51 eqtr4d ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → 𝑀 = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) )
53 52 fveq2d ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
54 40 53 eqtr2d ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 = 𝑏 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) )
55 54 3ad2antl1 ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) )
56 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
57 simpl1r ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑅 ∈ CRing )
58 14 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑁 ∈ Fin )
59 58 adantr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑁 ∈ Fin )
60 32 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
61 simpll2 ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
62 simpr ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑐 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
63 60 61 62 fovcdmd ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑐 ∈ 𝑁 ) → ( 𝑎 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
64 32 adantr ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
65 64 fovcdmda ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ ( 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) ) → ( 𝑑 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
66 65 3impb ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( 𝑑 𝑀 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
67 simpl3 ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑏 ∈ 𝑁 )
68 simpl2 ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑎 ∈ 𝑁 )
69 neqne ⊢ ( ¬ 𝑎 = 𝑏 → 𝑎 ≠ 𝑏 )
70 69 necomd ⊢ ( ¬ 𝑎 = 𝑏 → 𝑏 ≠ 𝑎 )
71 70 adantl ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → 𝑏 ≠ 𝑎 )
72 4 9 56 57 59 63 66 67 68 71 mdetralt2 ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
73 ifid ⊢ if ( 𝑑 = 𝑎 , ( 𝑑 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = ( 𝑑 𝑀 𝑐 )
74 oveq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 𝑀 𝑐 ) = ( 𝑎 𝑀 𝑐 ) )
75 74 adantl ⊢ ( ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) ∧ 𝑑 = 𝑎 ) → ( 𝑑 𝑀 𝑐 ) = ( 𝑎 𝑀 𝑐 ) )
76 75 ifeq1da ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → if ( 𝑑 = 𝑎 , ( 𝑑 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) )
77 73 76 eqtr3id ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝑑 𝑀 𝑐 ) = if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) )
78 77 ifeq2d ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) = if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) )
79 78 mpoeq3dv ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) = ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) )
80 79 fveq2d ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , if ( 𝑑 = 𝑎 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) ) )
81 iffalse ⊢ ( ¬ 𝑎 = 𝑏 → if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
82 81 adantl ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
83 72 80 82 3eqtr4d ⊢ ( ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) )
84 55 83 pm2.61dan ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑑 ∈ 𝑁 , 𝑐 ∈ 𝑁 ↦ if ( 𝑑 = 𝑏 , ( 𝑎 𝑀 𝑐 ) , ( 𝑑 𝑀 𝑐 ) ) ) ) = if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) )
85 38 84 eqtrd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑎 𝑀 𝑐 ) ( .r ‘ 𝑅 ) ( 𝑐 ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) ) ) = if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) )
86 85 mpoeq3dva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑎 𝑀 𝑐 ) ( .r ‘ 𝑅 ) ( 𝑐 ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) ) )
87 5 oveq2i ⊢ ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) )
88 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
89 88 adantl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
90 4 1 2 9 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
91 90 adantl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
92 91 19 ffvelcdmd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
93 1 9 7 56 matsc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) ) )
94 14 89 92 93 syl3anc ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) ) )
95 87 94 eqtrid ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 𝐷 ‘ 𝑀 ) , ( 0g ‘ 𝑅 ) ) ) )
96 86 95 eqtr4d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑐 ∈ 𝑁 ↦ ( ( 𝑎 𝑀 𝑐 ) ( .r ‘ 𝑅 ) ( 𝑐 ( 𝐽 ‘ 𝑀 ) 𝑏 ) ) ) ) ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )
97 23 27 96 3eqtr3d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑀 · ( 𝐽 ‘ 𝑀 ) ) = ( ( 𝐷 ‘ 𝑀 ) ∙ 1 ) )