MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  madurid Structured version   Visualization version   GIF version

Theorem madurid 22640
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.)
Hypotheses
Ref Expression
madurid.a 𝐴 = (𝑁 Mat 𝑅)
madurid.b 𝐵 = (Base‘𝐴)
madurid.j 𝐽 = (𝑁 maAdju 𝑅)
madurid.d 𝐷 = (𝑁 maDet 𝑅)
madurid.i 1 = (1r𝐴)
madurid.t · = (.r𝐴)
madurid.s = ( ·𝑠𝐴)
Assertion
Ref Expression
madurid ((𝑀𝐵𝑅 ∈ CRing) → (𝑀 · (𝐽𝑀)) = ((𝐷𝑀) 1 ))

Proof of Theorem madurid
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2736 . . 3 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
2 eqid 2736 . . 3 (Base‘𝑅) = (Base‘𝑅)
3 eqid 2736 . . 3 (.r𝑅) = (.r𝑅)
4 simpr 484 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑅 ∈ CRing)
5 madurid.a . . . . . 6 𝐴 = (𝑁 Mat 𝑅)
6 madurid.b . . . . . 6 𝐵 = (Base‘𝐴)
75, 6matrcl 22406 . . . . 5 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
87simpld 494 . . . 4 (𝑀𝐵𝑁 ∈ Fin)
98adantr 480 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑁 ∈ Fin)
105, 2, 6matbas2i 22418 . . . 4 (𝑀𝐵𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
1110adantr 480 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
12 madurid.j . . . . . . 7 𝐽 = (𝑁 maAdju 𝑅)
135, 12, 6maduf 22637 . . . . . 6 (𝑅 ∈ CRing → 𝐽:𝐵𝐵)
1413adantl 481 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝐽:𝐵𝐵)
15 simpl 482 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀𝐵)
1614, 15ffvelcdmd 7103 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → (𝐽𝑀) ∈ 𝐵)
175, 2, 6matbas2i 22418 . . . 4 ((𝐽𝑀) ∈ 𝐵 → (𝐽𝑀) ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
1816, 17syl 17 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝐽𝑀) ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
191, 2, 3, 4, 9, 9, 9, 11, 18mamuval 22387 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝐽𝑀)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))))
205, 1matmulr 22434 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
218, 20sylan 580 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
22 madurid.t . . . 4 · = (.r𝐴)
2321, 22eqtr4di 2794 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = · )
2423oveqd 7446 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝐽𝑀)) = (𝑀 · (𝐽𝑀)))
25 madurid.d . . . . . 6 𝐷 = (𝑁 maDet 𝑅)
26 simp1l 1198 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑀𝐵)
27 simp1r 1199 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑅 ∈ CRing)
28 elmapi 8885 . . . . . . . . . 10 (𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
2911, 28syl 17 . . . . . . . . 9 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
30293ad2ant1 1134 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3130adantr 480 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32 simpl2 1193 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑎𝑁)
33 simpr 484 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑐𝑁)
3431, 32, 33fovcdmd 7602 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅))
35 simp3 1139 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
365, 12, 6, 25, 3, 2, 26, 27, 34, 35madugsum 22639 . . . . 5 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏)))) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
37 iftrue 4530 . . . . . . . . 9 (𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (𝐷𝑀))
3837adantl 481 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (𝐷𝑀))
3929ffnd 6735 . . . . . . . . . . . 12 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 Fn (𝑁 × 𝑁))
40 fnov 7561 . . . . . . . . . . . 12 (𝑀 Fn (𝑁 × 𝑁) ↔ 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
4139, 40sylib 218 . . . . . . . . . . 11 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
4241adantr 480 . . . . . . . . . 10 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
43 equtr2 2026 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑏𝑑 = 𝑏) → 𝑎 = 𝑑)
4443oveq1d 7444 . . . . . . . . . . . . . 14 ((𝑎 = 𝑏𝑑 = 𝑏) → (𝑎𝑀𝑐) = (𝑑𝑀𝑐))
4544ifeq1da 4555 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐)))
46 ifid 4564 . . . . . . . . . . . . 13 if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)
4745, 46eqtrdi 2792 . . . . . . . . . . . 12 (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐))
4847adantl 481 . . . . . . . . . . 11 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐))
4948mpoeq3dv 7510 . . . . . . . . . 10 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
5042, 49eqtr4d 2779 . . . . . . . . 9 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))
5150fveq2d 6908 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷𝑀) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
5238, 51eqtr2d 2777 . . . . . . 7 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
53523ad2antl1 1186 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
54 eqid 2736 . . . . . . . 8 (0g𝑅) = (0g𝑅)
55 simpl1r 1226 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑅 ∈ CRing)
5693ad2ant1 1134 . . . . . . . . 9 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑁 ∈ Fin)
5756adantr 480 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑁 ∈ Fin)
5830ad2antrr 726 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
59 simpll2 1214 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑎𝑁)
60 simpr 484 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑐𝑁)
6158, 59, 60fovcdmd 7602 . . . . . . . 8 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅))
6230adantr 480 . . . . . . . . . 10 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
6362fovcdmda 7601 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ (𝑑𝑁𝑐𝑁)) → (𝑑𝑀𝑐) ∈ (Base‘𝑅))
64633impb 1115 . . . . . . . 8 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑𝑁𝑐𝑁) → (𝑑𝑀𝑐) ∈ (Base‘𝑅))
65 simpl3 1194 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏𝑁)
66 simpl2 1193 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑎𝑁)
67 neqne 2947 . . . . . . . . . 10 𝑎 = 𝑏𝑎𝑏)
6867necomd 2995 . . . . . . . . 9 𝑎 = 𝑏𝑏𝑎)
6968adantl 481 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏𝑎)
7025, 2, 54, 55, 57, 61, 64, 65, 66, 69mdetralt2 22605 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) = (0g𝑅))
71 ifid 4564 . . . . . . . . . . 11 if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)
72 oveq1 7436 . . . . . . . . . . . . 13 (𝑑 = 𝑎 → (𝑑𝑀𝑐) = (𝑎𝑀𝑐))
7372adantl 481 . . . . . . . . . . . 12 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑 = 𝑎) → (𝑑𝑀𝑐) = (𝑎𝑀𝑐))
7473ifeq1da 4555 . . . . . . . . . . 11 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))
7571, 74eqtr3id 2790 . . . . . . . . . 10 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑𝑀𝑐) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))
7675ifeq2d 4544 . . . . . . . . 9 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))
7776mpoeq3dv 7510 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
7877fveq2d 6908 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))))
79 iffalse 4533 . . . . . . . 8 𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (0g𝑅))
8079adantl 481 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (0g𝑅))
8170, 78, 803eqtr4d 2786 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8253, 81pm2.61dan 813 . . . . 5 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8336, 82eqtrd 2776 . . . 4 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8483mpoeq3dva 7508 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
85 madurid.i . . . . 5 1 = (1r𝐴)
8685oveq2i 7440 . . . 4 ((𝐷𝑀) 1 ) = ((𝐷𝑀) (1r𝐴))
87 crngring 20238 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
8887adantl 481 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝑅 ∈ Ring)
8925, 5, 6, 2mdetf 22591 . . . . . . 7 (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
9089adantl 481 . . . . . 6 ((𝑀𝐵𝑅 ∈ CRing) → 𝐷:𝐵⟶(Base‘𝑅))
9190, 15ffvelcdmd 7103 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → (𝐷𝑀) ∈ (Base‘𝑅))
92 madurid.s . . . . . 6 = ( ·𝑠𝐴)
935, 2, 92, 54matsc 22446 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐷𝑀) ∈ (Base‘𝑅)) → ((𝐷𝑀) (1r𝐴)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
949, 88, 91, 93syl3anc 1373 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → ((𝐷𝑀) (1r𝐴)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
9586, 94eqtrid 2788 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → ((𝐷𝑀) 1 ) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
9684, 95eqtr4d 2779 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))) = ((𝐷𝑀) 1 ))
9719, 24, 963eqtr3d 2784 1 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀 · (𝐽𝑀)) = ((𝐷𝑀) 1 ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2939  Vcvv 3479  ifcif 4524  cotp 4632  cmpt 5223   × cxp 5681   Fn wfn 6554  wf 6555  cfv 6559  (class class class)co 7429  cmpo 7431  m cmap 8862  Fincfn 8981  Basecbs 17243  .rcmulr 17294   ·𝑠 cvsca 17297  0gc0g 17480   Σg cgsu 17481  1rcur 20174  Ringcrg 20226  CRingccrg 20227   maMul cmmul 22384   Mat cmat 22401   maDet cmdat 22580   maAdju cmadu 22628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-cnex 11207  ax-resscn 11208  ax-1cn 11209  ax-icn 11210  ax-addcl 11211  ax-addrcl 11212  ax-mulcl 11213  ax-mulrcl 11214  ax-mulcom 11215  ax-addass 11216  ax-mulass 11217  ax-distr 11218  ax-i2m1 11219  ax-1ne0 11220  ax-1rid 11221  ax-rnegex 11222  ax-rrecex 11223  ax-cnre 11224  ax-pre-lttri 11225  ax-pre-lttrn 11226  ax-pre-ltadd 11227  ax-pre-mulgt0 11228  ax-addf 11230  ax-mulf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-ot 4633  df-uni 4906  df-int 4945  df-iun 4991  df-iin 4992  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-se 5636  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-of 7694  df-om 7884  df-1st 8010  df-2nd 8011  df-supp 8182  df-tpos 8247  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-2o 8503  df-er 8741  df-map 8864  df-pm 8865  df-ixp 8934  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-fsupp 9398  df-sup 9478  df-oi 9546  df-card 9975  df-pnf 11293  df-mnf 11294  df-xr 11295  df-ltxr 11296  df-le 11297  df-sub 11490  df-neg 11491  df-div 11917  df-nn 12263  df-2 12325  df-3 12326  df-4 12327  df-5 12328  df-6 12329  df-7 12330  df-8 12331  df-9 12332  df-n0 12523  df-xnn0 12596  df-z 12610  df-dec 12730  df-uz 12875  df-rp 13031  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-word 14549  df-lsw 14597  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-splice 14784  df-reverse 14793  df-s2 14883  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17244  df-ress 17271  df-plusg 17306  df-mulr 17307  df-starv 17308  df-sca 17309  df-vsca 17310  df-ip 17311  df-tset 17312  df-ple 17313  df-ds 17315  df-unif 17316  df-hom 17317  df-cco 17318  df-0g 17482  df-gsum 17483  df-prds 17488  df-pws 17490  df-mre 17625  df-mrc 17626  df-acs 17628  df-mgm 18649  df-sgrp 18728  df-mnd 18744  df-mhm 18792  df-submnd 18793  df-efmnd 18878  df-grp 18950  df-minusg 18951  df-sbg 18952  df-mulg 19082  df-subg 19137  df-ghm 19227  df-gim 19273  df-cntz 19331  df-oppg 19360  df-symg 19383  df-pmtr 19456  df-psgn 19505  df-evpm 19506  df-cmn 19796  df-abl 19797  df-mgp 20134  df-rng 20146  df-ur 20175  df-ring 20228  df-cring 20229  df-oppr 20326  df-dvdsr 20349  df-unit 20350  df-invr 20380  df-dvr 20393  df-rhm 20464  df-subrng 20538  df-subrg 20562  df-drng 20723  df-lmod 20852  df-lss 20922  df-sra 21164  df-rgmod 21165  df-cnfld 21357  df-zring 21450  df-zrh 21506  df-dsmm 21744  df-frlm 21759  df-mamu 22385  df-mat 22402  df-mdet 22581  df-madu 22630
This theorem is referenced by:  madulid  22641  matinv  22673  cpmadurid  22863  cpmidgsum2  22875
  Copyright terms: Public domain W3C validator