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

Metamath Proof Explorer

Theorem matinv

Description: The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in Lang p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses matinv.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matinv.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
matinv.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
matinv.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matinv.u ⊢ 𝑈 = ( Unit ‘ 𝐴 )
matinv.v ⊢ 𝑉 = ( Unit ‘ 𝑅 )
matinv.h ⊢ 𝐻 = ( invr ‘ 𝑅 )
matinv.i ⊢ 𝐼 = ( invr ‘ 𝐴 )
matinv.t ⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
Assertion matinv ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ∈ 𝑈 ∧ ( 𝐼 ‘ 𝑀 ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 matinv.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matinv.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
3 matinv.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4 matinv.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 matinv.u ⊢ 𝑈 = ( Unit ‘ 𝐴 )
6 matinv.v ⊢ 𝑉 = ( Unit ‘ 𝑅 )
7 matinv.h ⊢ 𝐻 = ( invr ‘ 𝑅 )
8 matinv.i ⊢ 𝐼 = ( invr ‘ 𝐴 )
9 matinv.t ⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
10 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
11 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
12 1 4 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
13 12 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
14 13 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑁 ∈ Fin )
15 simp1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑅 ∈ CRing )
16 1 matassa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ AssAlg )
17 14 15 16 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝐴 ∈ AssAlg )
18 assaring ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ Ring )
19 17 18 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝐴 ∈ Ring )
20 simp2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑀 ∈ 𝐵 )
21 assalmod ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ LMod )
22 17 21 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝐴 ∈ LMod )
23 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
24 23 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑅 ∈ Ring )
25 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 )
26 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 6 7 26 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑅 ) )
28 24 25 27 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑅 ) )
29 1 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
30 14 15 29 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
31 30 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
32 28 31 eleqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
33 1 2 4 maduf ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
34 33 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → 𝐽 : 𝐵 ⟶ 𝐵 )
35 34 20 ffvelcdmd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
36 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
37 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
38 4 36 9 37 lmodvscl ⊢ ( ( 𝐴 ∈ LMod ∧ ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ∈ 𝐵 )
39 22 32 35 38 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ∈ 𝐵 )
40 4 36 37 9 10 assaassr ⊢ ( ( 𝐴 ∈ AssAlg ∧ ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 ) ) → ( 𝑀 ( .r ‘ 𝐴 ) ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝑀 ( .r ‘ 𝐴 ) ( 𝐽 ‘ 𝑀 ) ) ) )
41 17 32 20 35 40 syl13anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ( .r ‘ 𝐴 ) ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝑀 ( .r ‘ 𝐴 ) ( 𝐽 ‘ 𝑀 ) ) ) )
42 1 4 2 3 11 10 9 madurid ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( 𝑀 ( .r ‘ 𝐴 ) ( 𝐽 ‘ 𝑀 ) ) = ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) )
43 20 15 42 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ( .r ‘ 𝐴 ) ( 𝐽 ‘ 𝑀 ) ) = ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) )
44 43 oveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝑀 ( .r ‘ 𝐴 ) ( 𝐽 ‘ 𝑀 ) ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) ) )
45 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
46 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
47 6 7 45 46 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) = ( 1r ‘ 𝑅 ) )
48 24 25 47 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) = ( 1r ‘ 𝑅 ) )
49 30 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝐴 ) ) )
50 49 oveqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ 𝑅 ) ( 𝐷 ‘ 𝑀 ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ ( Scalar ‘ 𝐴 ) ) ( 𝐷 ‘ 𝑀 ) ) )
51 30 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) )
52 48 50 51 3eqtr3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ ( Scalar ‘ 𝐴 ) ) ( 𝐷 ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) )
53 52 oveq1d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ ( Scalar ‘ 𝐴 ) ) ( 𝐷 ‘ 𝑀 ) ) ∙ ( 1r ‘ 𝐴 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∙ ( 1r ‘ 𝐴 ) ) )
54 26 6 unitcl ⊢ ( ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
55 54 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
56 55 31 eleqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
57 4 11 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
58 19 57 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
59 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝐴 ) ) = ( .r ‘ ( Scalar ‘ 𝐴 ) )
60 4 36 9 37 59 lmodvsass ⊢ ( ( 𝐴 ∈ LMod ∧ ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ 𝑀 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ ( Scalar ‘ 𝐴 ) ) ( 𝐷 ‘ 𝑀 ) ) ∙ ( 1r ‘ 𝐴 ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) ) )
61 22 32 56 58 60 syl13anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ( .r ‘ ( Scalar ‘ 𝐴 ) ) ( 𝐷 ‘ 𝑀 ) ) ∙ ( 1r ‘ 𝐴 ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) ) )
62 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝐴 ) ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) )
63 4 36 9 62 lmodvs1 ⊢ ( ( 𝐴 ∈ LMod ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∙ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐴 ) )
64 22 58 63 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∙ ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐴 ) )
65 53 61 64 3eqtr3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) ) = ( 1r ‘ 𝐴 ) )
66 41 44 65 3eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ( .r ‘ 𝐴 ) ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ) = ( 1r ‘ 𝐴 ) )
67 4 36 37 9 10 assaass ⊢ ( ( 𝐴 ∈ AssAlg ∧ ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 ∧ 𝑀 ∈ 𝐵 ) ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑀 ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐽 ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) )
68 17 32 35 20 67 syl13anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑀 ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐽 ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) )
69 1 4 2 3 11 10 9 madulid ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing ) → ( ( 𝐽 ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) )
70 20 15 69 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐽 ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) = ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) )
71 70 oveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐽 ‘ 𝑀 ) ( .r ‘ 𝐴 ) 𝑀 ) ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( ( 𝐷 ‘ 𝑀 ) ∙ ( 1r ‘ 𝐴 ) ) ) )
72 68 71 65 3eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑀 ) = ( 1r ‘ 𝐴 ) )
73 4 10 11 5 8 19 20 39 66 72 invrvald ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝑀 ) ∈ 𝑉 ) → ( 𝑀 ∈ 𝑈 ∧ ( 𝐼 ‘ 𝑀 ) = ( ( 𝐻 ‘ ( 𝐷 ‘ 𝑀 ) ) ∙ ( 𝐽 ‘ 𝑀 ) ) ) )