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

Theorem madurid 21228
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 2821 . . 3 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
2 eqid 2821 . . 3 (Base‘𝑅) = (Base‘𝑅)
3 eqid 2821 . . 3 (.r𝑅) = (.r𝑅)
4 simpr 488 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑅 ∈ CRing)
5 madurid.a . . . . . 6 𝐴 = (𝑁 Mat 𝑅)
6 madurid.b . . . . . 6 𝐵 = (Base‘𝐴)
75, 6matrcl 20996 . . . . 5 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
87simpld 498 . . . 4 (𝑀𝐵𝑁 ∈ Fin)
98adantr 484 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑁 ∈ Fin)
105, 2, 6matbas2i 21006 . . . 4 (𝑀𝐵𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
1110adantr 484 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
12 madurid.j . . . . . . 7 𝐽 = (𝑁 maAdju 𝑅)
135, 12, 6maduf 21225 . . . . . 6 (𝑅 ∈ CRing → 𝐽:𝐵𝐵)
1413adantl 485 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝐽:𝐵𝐵)
15 simpl 486 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀𝐵)
1614, 15ffvelrnd 6825 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → (𝐽𝑀) ∈ 𝐵)
175, 2, 6matbas2i 21006 . . . 4 ((𝐽𝑀) ∈ 𝐵 → (𝐽𝑀) ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
1816, 17syl 17 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝐽𝑀) ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
191, 2, 3, 4, 9, 9, 9, 11, 18mamuval 20972 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝐽𝑀)) = (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))))
205, 1matmulr 21022 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
218, 20sylan 583 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
22 madurid.t . . . 4 · = (.r𝐴)
2321, 22syl6eqr 2874 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = · )
2423oveqd 7147 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)(𝐽𝑀)) = (𝑀 · (𝐽𝑀)))
25 madurid.d . . . . . 6 𝐷 = (𝑁 maDet 𝑅)
26 simp1l 1194 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑀𝐵)
27 simp1r 1195 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑅 ∈ CRing)
28 elmapi 8403 . . . . . . . . . 10 (𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
2911, 28syl 17 . . . . . . . . 9 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
30293ad2ant1 1130 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3130adantr 484 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32 simpl2 1189 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑎𝑁)
33 simpr 488 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → 𝑐𝑁)
3431, 32, 33fovrnd 7295 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑐𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅))
35 simp3 1135 . . . . . 6 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
365, 12, 6, 25, 3, 2, 26, 27, 34, 35madugsum 21227 . . . . 5 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏)))) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
37 iftrue 4446 . . . . . . . . 9 (𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (𝐷𝑀))
3837adantl 485 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (𝐷𝑀))
3929ffnd 6488 . . . . . . . . . . . 12 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 Fn (𝑁 × 𝑁))
40 fnov 7256 . . . . . . . . . . . 12 (𝑀 Fn (𝑁 × 𝑁) ↔ 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
4139, 40sylib 221 . . . . . . . . . . 11 ((𝑀𝐵𝑅 ∈ CRing) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
4241adantr 484 . . . . . . . . . 10 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
43 equtr2 2035 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑏𝑑 = 𝑏) → 𝑎 = 𝑑)
4443oveq1d 7145 . . . . . . . . . . . . . 14 ((𝑎 = 𝑏𝑑 = 𝑏) → (𝑎𝑀𝑐) = (𝑑𝑀𝑐))
4544ifeq1da 4470 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐)))
46 ifid 4479 . . . . . . . . . . . . 13 if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)
4745, 46syl6eq 2872 . . . . . . . . . . . 12 (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐))
4847adantl 485 . . . . . . . . . . 11 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐))
4948mpoeq3dv 7207 . . . . . . . . . 10 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑𝑁, 𝑐𝑁 ↦ (𝑑𝑀𝑐)))
5042, 49eqtr4d 2859 . . . . . . . . 9 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))
5150fveq2d 6647 . . . . . . . 8 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷𝑀) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
5238, 51eqtr2d 2857 . . . . . . 7 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
53523ad2antl1 1182 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
54 eqid 2821 . . . . . . . 8 (0g𝑅) = (0g𝑅)
55 simpl1r 1222 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑅 ∈ CRing)
5693ad2ant1 1130 . . . . . . . . 9 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → 𝑁 ∈ Fin)
5756adantr 484 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑁 ∈ Fin)
5830ad2antrr 725 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
59 simpll2 1210 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑎𝑁)
60 simpr 488 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → 𝑐𝑁)
6158, 59, 60fovrnd 7295 . . . . . . . 8 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅))
6230adantr 484 . . . . . . . . . 10 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
6362fovrnda 7294 . . . . . . . . 9 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ (𝑑𝑁𝑐𝑁)) → (𝑑𝑀𝑐) ∈ (Base‘𝑅))
64633impb 1112 . . . . . . . 8 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑𝑁𝑐𝑁) → (𝑑𝑀𝑐) ∈ (Base‘𝑅))
65 simpl3 1190 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏𝑁)
66 simpl2 1189 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑎𝑁)
67 neqne 3015 . . . . . . . . . 10 𝑎 = 𝑏𝑎𝑏)
6867necomd 3062 . . . . . . . . 9 𝑎 = 𝑏𝑏𝑎)
6968adantl 485 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏𝑎)
7025, 2, 54, 55, 57, 61, 64, 65, 66, 69mdetralt2 21193 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) = (0g𝑅))
71 ifid 4479 . . . . . . . . . . 11 if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)
72 oveq1 7137 . . . . . . . . . . . . 13 (𝑑 = 𝑎 → (𝑑𝑀𝑐) = (𝑎𝑀𝑐))
7372adantl 485 . . . . . . . . . . . 12 (((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑 = 𝑎) → (𝑑𝑀𝑐) = (𝑎𝑀𝑐))
7473ifeq1da 4470 . . . . . . . . . . 11 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))
7571, 74syl5eqr 2870 . . . . . . . . . 10 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑𝑀𝑐) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))
7675ifeq2d 4459 . . . . . . . . 9 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))
7776mpoeq3dv 7207 . . . . . . . 8 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))
7877fveq2d 6647 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))))
79 iffalse 4449 . . . . . . . 8 𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (0g𝑅))
8079adantl 485 . . . . . . 7 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)) = (0g𝑅))
8170, 78, 803eqtr4d 2866 . . . . . 6 ((((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8253, 81pm2.61dan 812 . . . . 5 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝐷‘(𝑑𝑁, 𝑐𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8336, 82eqtrd 2856 . . . 4 (((𝑀𝐵𝑅 ∈ CRing) ∧ 𝑎𝑁𝑏𝑁) → (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏)))) = if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅)))
8483mpoeq3dva 7205 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
85 madurid.i . . . . 5 1 = (1r𝐴)
8685oveq2i 7141 . . . 4 ((𝐷𝑀) 1 ) = ((𝐷𝑀) (1r𝐴))
87 crngring 19286 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
8887adantl 485 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → 𝑅 ∈ Ring)
8925, 5, 6, 2mdetf 21179 . . . . . . 7 (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
9089adantl 485 . . . . . 6 ((𝑀𝐵𝑅 ∈ CRing) → 𝐷:𝐵⟶(Base‘𝑅))
9190, 15ffvelrnd 6825 . . . . 5 ((𝑀𝐵𝑅 ∈ CRing) → (𝐷𝑀) ∈ (Base‘𝑅))
92 madurid.s . . . . . 6 = ( ·𝑠𝐴)
935, 2, 92, 54matsc 21034 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐷𝑀) ∈ (Base‘𝑅)) → ((𝐷𝑀) (1r𝐴)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
949, 88, 91, 93syl3anc 1368 . . . 4 ((𝑀𝐵𝑅 ∈ CRing) → ((𝐷𝑀) (1r𝐴)) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
9586, 94syl5eq 2868 . . 3 ((𝑀𝐵𝑅 ∈ CRing) → ((𝐷𝑀) 1 ) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝑏, (𝐷𝑀), (0g𝑅))))
9684, 95eqtr4d 2859 . 2 ((𝑀𝐵𝑅 ∈ CRing) → (𝑎𝑁, 𝑏𝑁 ↦ (𝑅 Σg (𝑐𝑁 ↦ ((𝑎𝑀𝑐)(.r𝑅)(𝑐(𝐽𝑀)𝑏))))) = ((𝐷𝑀) 1 ))
9719, 24, 963eqtr3d 2864 1 ((𝑀𝐵𝑅 ∈ CRing) → (𝑀 · (𝐽𝑀)) = ((𝐷𝑀) 1 ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  wne 3007  Vcvv 3471  ifcif 4440  cotp 4548  cmpt 5119   × cxp 5526   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7130  cmpo 7132  m cmap 8381  Fincfn 8484  Basecbs 16461  .rcmulr 16544   ·𝑠 cvsca 16547  0gc0g 16691   Σg cgsu 16692  1rcur 19229  Ringcrg 19275  CRingccrg 19276   maMul cmmul 20969   Mat cmat 20991   maDet cmdat 21168   maAdju cmadu 21216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-addf 10593  ax-mulf 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-ot 4549  df-uni 4812  df-int 4850  df-iun 4894  df-iin 4895  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-of 7384  df-om 7556  df-1st 7664  df-2nd 7665  df-supp 7806  df-tpos 7867  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-2o 8078  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-ixp 8437  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-fsupp 8810  df-sup 8882  df-oi 8950  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-4 11680  df-5 11681  df-6 11682  df-7 11683  df-8 11684  df-9 11685  df-n0 11876  df-xnn0 11946  df-z 11960  df-dec 12077  df-uz 12222  df-rp 12368  df-fz 12876  df-fzo 13017  df-seq 13353  df-exp 13414  df-hash 13675  df-word 13846  df-lsw 13894  df-concat 13902  df-s1 13929  df-substr 13982  df-pfx 14012  df-splice 14091  df-reverse 14100  df-s2 14189  df-struct 16463  df-ndx 16464  df-slot 16465  df-base 16467  df-sets 16468  df-ress 16469  df-plusg 16556  df-mulr 16557  df-starv 16558  df-sca 16559  df-vsca 16560  df-ip 16561  df-tset 16562  df-ple 16563  df-ds 16565  df-unif 16566  df-hom 16567  df-cco 16568  df-0g 16693  df-gsum 16694  df-prds 16699  df-pws 16701  df-mre 16835  df-mrc 16836  df-acs 16838  df-mgm 17830  df-sgrp 17879  df-mnd 17890  df-mhm 17934  df-submnd 17935  df-efmnd 18012  df-grp 18084  df-minusg 18085  df-sbg 18086  df-mulg 18203  df-subg 18254  df-ghm 18334  df-gim 18377  df-cntz 18425  df-oppg 18452  df-symg 18474  df-pmtr 18548  df-psgn 18597  df-evpm 18598  df-cmn 18886  df-abl 18887  df-mgp 19218  df-ur 19230  df-ring 19277  df-cring 19278  df-oppr 19351  df-dvdsr 19369  df-unit 19370  df-invr 19400  df-dvr 19411  df-rnghom 19445  df-drng 19479  df-subrg 19508  df-lmod 19611  df-lss 19679  df-sra 19919  df-rgmod 19920  df-cnfld 20521  df-zring 20593  df-zrh 20626  df-dsmm 20851  df-frlm 20866  df-mamu 20970  df-mat 20992  df-mdet 21169  df-madu 21218
This theorem is referenced by:  madulid  21229  matinv  21261  cpmadurid  21450  cpmidgsum2  21462
  Copyright terms: Public domain W3C validator