Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) |
2 | | eqid 2622 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2622 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | simpr 477 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing) |
5 | | madurid.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
6 | | madurid.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
7 | 5, 6 | matrcl 20218 |
. . . . 5
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
8 | 7 | simpld 475 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → 𝑁 ∈ Fin) |
9 | 8 | adantr 481 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑁 ∈ Fin) |
10 | 5, 2, 6 | matbas2i 20228 |
. . . 4
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
11 | 10 | adantr 481 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
12 | | madurid.j |
. . . . . . 7
⊢ 𝐽 = (𝑁 maAdju 𝑅) |
13 | 5, 12, 6 | maduf 20447 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵) |
14 | 13 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝐽:𝐵⟶𝐵) |
15 | | simpl 473 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑀 ∈ 𝐵) |
16 | 14, 15 | ffvelrnd 6360 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝐽‘𝑀) ∈ 𝐵) |
17 | 5, 2, 6 | matbas2i 20228 |
. . . 4
⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝐽‘𝑀) ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁))) |
19 | 1, 2, 3, 4, 9, 9, 9, 11, 18 | mamuval 20192 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑀(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐽‘𝑀)) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑅 Σg (𝑐 ∈ 𝑁 ↦ ((𝑎𝑀𝑐)(.r‘𝑅)(𝑐(𝐽‘𝑀)𝑏)))))) |
20 | 5, 1 | matmulr 20244 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
21 | 8, 20 | sylan 488 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
22 | | madurid.t |
. . . 4
⊢ · =
(.r‘𝐴) |
23 | 21, 22 | syl6eqr 2674 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = · ) |
24 | 23 | oveqd 6667 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑀(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)(𝐽‘𝑀)) = (𝑀 · (𝐽‘𝑀))) |
25 | | madurid.d |
. . . . . 6
⊢ 𝐷 = (𝑁 maDet 𝑅) |
26 | | simp1l 1085 |
. . . . . 6
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑀 ∈ 𝐵) |
27 | | simp1r 1086 |
. . . . . 6
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ CRing) |
28 | | elmapi 7879 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ((Base‘𝑅) ↑𝑚
(𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
29 | 11, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
30 | 29 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ 𝑐 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
32 | | simpl2 1065 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ 𝑐 ∈ 𝑁) → 𝑎 ∈ 𝑁) |
33 | | simpr 477 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
34 | 31, 32, 33 | fovrnd 6806 |
. . . . . 6
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ 𝑐 ∈ 𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅)) |
35 | | simp3 1063 |
. . . . . 6
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁) |
36 | 5, 12, 6, 25, 3, 2,
26, 27, 34, 35 | madugsum 20449 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑅 Σg (𝑐 ∈ 𝑁 ↦ ((𝑎𝑀𝑐)(.r‘𝑅)(𝑐(𝐽‘𝑀)𝑏)))) = (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) |
37 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)) = (𝐷‘𝑀)) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)) = (𝐷‘𝑀)) |
39 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅) → 𝑀 Fn (𝑁 × 𝑁)) |
40 | 29, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑀 Fn (𝑁 × 𝑁)) |
41 | | fnov 6768 |
. . . . . . . . . . . 12
⊢ (𝑀 Fn (𝑁 × 𝑁) ↔ 𝑀 = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ (𝑑𝑀𝑐))) |
42 | 40, 41 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑀 = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ (𝑑𝑀𝑐))) |
43 | 42 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ (𝑑𝑀𝑐))) |
44 | | equtr2 1954 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑏 ∧ 𝑑 = 𝑏) → 𝑎 = 𝑑) |
45 | 44 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑏 ∧ 𝑑 = 𝑏) → (𝑎𝑀𝑐) = (𝑑𝑀𝑐)) |
46 | 45 | ifeq1da 4116 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐))) |
47 | | ifid 4125 |
. . . . . . . . . . . . 13
⊢ if(𝑑 = 𝑏, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐) |
48 | 46, 47 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)) |
49 | 48 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐)) |
50 | 49 | mpt2eq3dv 6721 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ (𝑑𝑀𝑐))) |
51 | 43, 50 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → 𝑀 = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) |
52 | 51 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷‘𝑀) = (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) |
53 | 38, 52 | eqtr2d 2657 |
. . . . . . 7
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅))) |
54 | 53 | 3ad2antl1 1223 |
. . . . . 6
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ 𝑎 = 𝑏) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅))) |
55 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
56 | | simpl1r 1113 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑅 ∈ CRing) |
57 | 9 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑁 ∈ Fin) |
58 | 57 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑁 ∈ Fin) |
59 | 30 | ad2antrr 762 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
60 | | simpll2 1101 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐 ∈ 𝑁) → 𝑎 ∈ 𝑁) |
61 | | simpr 477 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁) |
62 | 59, 60, 61 | fovrnd 6806 |
. . . . . . . 8
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑐 ∈ 𝑁) → (𝑎𝑀𝑐) ∈ (Base‘𝑅)) |
63 | 30 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) |
64 | 63 | fovrnda 6805 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ (𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁)) → (𝑑𝑀𝑐) ∈ (Base‘𝑅)) |
65 | 64 | 3impb 1260 |
. . . . . . . 8
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → (𝑑𝑀𝑐) ∈ (Base‘𝑅)) |
66 | | simpl3 1066 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏 ∈ 𝑁) |
67 | | simpl2 1065 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑎 ∈ 𝑁) |
68 | | df-ne 2795 |
. . . . . . . . . . 11
⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏) |
69 | 68 | biimpri 218 |
. . . . . . . . . 10
⊢ (¬
𝑎 = 𝑏 → 𝑎 ≠ 𝑏) |
70 | 69 | necomd 2849 |
. . . . . . . . 9
⊢ (¬
𝑎 = 𝑏 → 𝑏 ≠ 𝑎) |
71 | 70 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → 𝑏 ≠ 𝑎) |
72 | 25, 2, 55, 56, 58, 62, 65, 66, 67, 71 | mdetralt2 20415 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) = (0g‘𝑅)) |
73 | | ifid 4125 |
. . . . . . . . . . 11
⊢ if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = (𝑑𝑀𝑐) |
74 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑎 → (𝑑𝑀𝑐) = (𝑎𝑀𝑐)) |
75 | 74 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) ∧ 𝑑 = 𝑎) → (𝑑𝑀𝑐) = (𝑎𝑀𝑐)) |
76 | 75 | ifeq1da 4116 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑎, (𝑑𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) |
77 | 73, 76 | syl5eqr 2670 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑𝑀𝑐) = if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) |
78 | 77 | ifeq2d 4105 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)) = if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) |
79 | 78 | mpt2eq3dv 6721 |
. . . . . . . 8
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐))) = (𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐))))) |
80 | 79 | fveq2d 6195 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), if(𝑑 = 𝑎, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))))) |
81 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑎 = 𝑏 → if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)) = (0g‘𝑅)) |
82 | 81 | adantl 482 |
. . . . . . 7
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)) = (0g‘𝑅)) |
83 | 72, 80, 82 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) ∧ ¬ 𝑎 = 𝑏) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅))) |
84 | 54, 83 | pm2.61dan 832 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝐷‘(𝑑 ∈ 𝑁, 𝑐 ∈ 𝑁 ↦ if(𝑑 = 𝑏, (𝑎𝑀𝑐), (𝑑𝑀𝑐)))) = if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅))) |
85 | 36, 84 | eqtrd 2656 |
. . . 4
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑅 Σg (𝑐 ∈ 𝑁 ↦ ((𝑎𝑀𝑐)(.r‘𝑅)(𝑐(𝐽‘𝑀)𝑏)))) = if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅))) |
86 | 85 | mpt2eq3dva 6719 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑅 Σg (𝑐 ∈ 𝑁 ↦ ((𝑎𝑀𝑐)(.r‘𝑅)(𝑐(𝐽‘𝑀)𝑏))))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)))) |
87 | | madurid.i |
. . . . 5
⊢ 1 =
(1r‘𝐴) |
88 | 87 | oveq2i 6661 |
. . . 4
⊢ ((𝐷‘𝑀) ∙ 1 ) = ((𝐷‘𝑀) ∙
(1r‘𝐴)) |
89 | | crngring 18558 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
90 | 89 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
91 | 25, 5, 6, 2 | mdetf 20401 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅)) |
92 | 91 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → 𝐷:𝐵⟶(Base‘𝑅)) |
93 | 92, 15 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝐷‘𝑀) ∈ (Base‘𝑅)) |
94 | | madurid.s |
. . . . . 6
⊢ ∙ = (
·𝑠 ‘𝐴) |
95 | 5, 2, 94, 55 | matsc 20256 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐷‘𝑀) ∈ (Base‘𝑅)) → ((𝐷‘𝑀) ∙
(1r‘𝐴)) =
(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)))) |
96 | 9, 90, 93, 95 | syl3anc 1326 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → ((𝐷‘𝑀) ∙
(1r‘𝐴)) =
(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)))) |
97 | 88, 96 | syl5eq 2668 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → ((𝐷‘𝑀) ∙ 1 ) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝑏, (𝐷‘𝑀), (0g‘𝑅)))) |
98 | 86, 97 | eqtr4d 2659 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ (𝑅 Σg (𝑐 ∈ 𝑁 ↦ ((𝑎𝑀𝑐)(.r‘𝑅)(𝑐(𝐽‘𝑀)𝑏))))) = ((𝐷‘𝑀) ∙ 1 )) |
99 | 19, 24, 98 | 3eqtr3d 2664 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑀 · (𝐽‘𝑀)) = ((𝐷‘𝑀) ∙ 1 )) |