| Step | Hyp | Ref
| Expression |
| 1 | | mpteq1 5235 |
. . . . 5
⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) |
| 2 | 1 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = ∅ → (𝑅 Σg
(𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))) |
| 3 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅)) |
| 4 | 3 | ifbid 4549 |
. . . . . . 7
⊢ (𝑐 = ∅ → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 5 | 4 | ifeq1d 4545 |
. . . . . 6
⊢ (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 6 | 5 | mpoeq3dv 7512 |
. . . . 5
⊢ (𝑐 = ∅ → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) |
| 7 | 6 | fveq2d 6910 |
. . . 4
⊢ (𝑐 = ∅ → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 8 | 2, 7 | eqeq12d 2753 |
. . 3
⊢ (𝑐 = ∅ → ((𝑅 Σg
(𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 9 | | mpteq1 5235 |
. . . . 5
⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) |
| 10 | 9 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = 𝑑 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))) |
| 11 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑)) |
| 12 | 11 | ifbid 4549 |
. . . . . . 7
⊢ (𝑐 = 𝑑 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 13 | 12 | ifeq1d 4545 |
. . . . . 6
⊢ (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 14 | 13 | mpoeq3dv 7512 |
. . . . 5
⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) |
| 15 | 14 | fveq2d 6910 |
. . . 4
⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 16 | 10, 15 | eqeq12d 2753 |
. . 3
⊢ (𝑐 = 𝑑 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 17 | | mpteq1 5235 |
. . . . 5
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) |
| 18 | 17 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))) |
| 19 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ (𝑑 ∪ {𝑒}))) |
| 20 | 19 | ifbid 4549 |
. . . . . . 7
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 21 | 20 | ifeq1d 4545 |
. . . . . 6
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 22 | 21 | mpoeq3dv 7512 |
. . . . 5
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) |
| 23 | 22 | fveq2d 6910 |
. . . 4
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 24 | 18, 23 | eqeq12d 2753 |
. . 3
⊢ (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 25 | | mpteq1 5235 |
. . . . 5
⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) |
| 26 | 25 | oveq2d 7447 |
. . . 4
⊢ (𝑐 = 𝑁 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))) |
| 27 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁)) |
| 28 | 27 | ifbid 4549 |
. . . . . . 7
⊢ (𝑐 = 𝑁 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 29 | 28 | ifeq1d 4545 |
. . . . . 6
⊢ (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 30 | 29 | mpoeq3dv 7512 |
. . . . 5
⊢ (𝑐 = 𝑁 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) |
| 31 | 30 | fveq2d 6910 |
. . . 4
⊢ (𝑐 = 𝑁 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 32 | 26, 31 | eqeq12d 2753 |
. . 3
⊢ (𝑐 = 𝑁 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 33 | | mpt0 6710 |
. . . . . 6
⊢ (𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = ∅ |
| 34 | 33 | oveq2i 7442 |
. . . . 5
⊢ (𝑅 Σg
(𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg
∅) |
| 35 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 36 | 35 | gsum0 18697 |
. . . . 5
⊢ (𝑅 Σg
∅) = (0g‘𝑅) |
| 37 | 34, 36 | eqtri 2765 |
. . . 4
⊢ (𝑅 Σg
(𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (0g‘𝑅) |
| 38 | | noel 4338 |
. . . . . . . . 9
⊢ ¬
𝑏 ∈
∅ |
| 39 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
𝑏 ∈ ∅ →
if(𝑏 ∈ ∅,
⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅)) |
| 40 | 38, 39 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅)) |
| 41 | 40 | ifeq1d 4545 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏))) |
| 42 | 41 | mpoeq3ia 7511 |
. . . . . 6
⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏))) |
| 43 | 42 | fveq2i 6909 |
. . . . 5
⊢ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))) |
| 44 | | madugsum.d |
. . . . . 6
⊢ 𝐷 = (𝑁 maDet 𝑅) |
| 45 | | madugsum.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑅) |
| 46 | | madugsum.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 47 | | madugsum.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ 𝐵) |
| 48 | | maduf.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 49 | | maduf.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐴) |
| 50 | 48, 49 | matrcl 22416 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 51 | 47, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
| 52 | 51 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 53 | 48, 45, 49 | matbas2i 22428 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁))) |
| 54 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾) |
| 55 | 47, 53, 54 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:(𝑁 × 𝑁)⟶𝐾) |
| 56 | 55 | fovcdmda 7604 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾) |
| 57 | 56 | 3impb 1115 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾) |
| 58 | | madugsum.l |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ 𝑁) |
| 59 | 44, 45, 35, 46, 52, 57, 58 | mdetr0 22611 |
. . . . 5
⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))) = (0g‘𝑅)) |
| 60 | 43, 59 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (0g‘𝑅)) |
| 61 | 37, 60 | eqtr4id 2796 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ ∅ ↦
(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 62 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 63 | 46 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CRing) |
| 64 | | crngring 20242 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 65 | 63, 64 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Ring) |
| 66 | | ringcmn 20279 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CMnd) |
| 68 | 52 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑁 ∈ Fin) |
| 69 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ⊆ 𝑁) |
| 70 | 68, 69 | ssfid 9301 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ∈ Fin) |
| 71 | 65 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑅 ∈ Ring) |
| 72 | 69 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑏 ∈ 𝑁) |
| 73 | | madugsum.x |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾) |
| 74 | 73 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) |
| 75 | 74 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) |
| 76 | | rspcsbela 4438 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾) |
| 77 | 72, 75, 76 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾) |
| 78 | | maduf.j |
. . . . . . . . . . . . . 14
⊢ 𝐽 = (𝑁 maAdju 𝑅) |
| 79 | 48, 78, 49 | maduf 22647 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵) |
| 80 | 46, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽:𝐵⟶𝐵) |
| 81 | 80, 47 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽‘𝑀) ∈ 𝐵) |
| 82 | 48, 45, 49 | matbas2i 22428 |
. . . . . . . . . . 11
⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁))) |
| 83 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ ((𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾) |
| 84 | 81, 82, 83 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾) |
| 85 | 84 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾) |
| 86 | 58 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝐿 ∈ 𝑁) |
| 87 | 85, 72, 86 | fovcdmd 7605 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) |
| 88 | | madugsum.t |
. . . . . . . . 9
⊢ · =
(.r‘𝑅) |
| 89 | 45, 88 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾) |
| 90 | 71, 77, 87, 89 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾) |
| 91 | | vex 3484 |
. . . . . . . 8
⊢ 𝑒 ∈ V |
| 92 | 91 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ V) |
| 93 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → ¬ 𝑒 ∈ 𝑑) |
| 94 | 93 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ 𝑒 ∈ 𝑑) |
| 95 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → 𝑒 ∈ 𝑁) |
| 96 | 95 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ 𝑁) |
| 97 | 74 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) |
| 98 | | rspcsbela 4438 |
. . . . . . . . 9
⊢ ((𝑒 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) |
| 99 | 96, 97, 98 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) |
| 100 | 84 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾) |
| 101 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝐿 ∈ 𝑁) |
| 102 | 100, 96, 101 | fovcdmd 7605 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) |
| 103 | 45, 88 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾) |
| 104 | 65, 99, 102, 103 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾) |
| 105 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑏 = 𝑒 → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋) |
| 106 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑏 = 𝑒 → (𝑏(𝐽‘𝑀)𝐿) = (𝑒(𝐽‘𝑀)𝐿)) |
| 107 | 105, 106 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑏 = 𝑒 → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) |
| 108 | 45, 62, 67, 70, 90, 92, 94, 104, 107 | gsumunsn 19978 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))) |
| 109 | 108 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))) |
| 110 | | oveq1 7438 |
. . . . . 6
⊢ ((𝑅 Σg
(𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))) |
| 111 | 110 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))) |
| 112 | | elun 4153 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒})) |
| 113 | | velsn 4642 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒) |
| 114 | 113 | orbi2i 913 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) |
| 115 | 112, 114 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) |
| 116 | | ifbi 4548 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 117 | 115, 116 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) |
| 118 | | ringmnd 20240 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
| 119 | 65, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Mnd) |
| 120 | 119 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ Mnd) |
| 121 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁) |
| 122 | 97 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) |
| 123 | 121, 122,
76 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾) |
| 124 | | elequ1 2115 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑒 → (𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑)) |
| 125 | 124 | biimpac 478 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒) → 𝑒 ∈ 𝑑) |
| 126 | 94, 125 | nsyl 140 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) |
| 127 | 126 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) |
| 128 | 45, 35, 62 | mndifsplit 22642 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Mnd ∧
⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))) |
| 129 | 120, 123,
127, 128 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))) |
| 130 | 117, 129 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))) |
| 131 | 105 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 = 𝑒) → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋) |
| 132 | 131 | ifeq1da 4557 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 133 | | ovif2 7532 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑒 /
𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 ·
(1r‘𝑅)),
(⦋𝑒 / 𝑖⦌𝑋 ·
(0g‘𝑅))) |
| 134 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 135 | 45, 88, 134 | ringridm 20267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 ·
(1r‘𝑅)) =
⦋𝑒 / 𝑖⦌𝑋) |
| 136 | 65, 99, 135 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 ·
(1r‘𝑅)) =
⦋𝑒 / 𝑖⦌𝑋) |
| 137 | 45, 88, 35 | ringrz 20291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 ·
(0g‘𝑅)) =
(0g‘𝑅)) |
| 138 | 65, 99, 137 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 ·
(0g‘𝑅)) =
(0g‘𝑅)) |
| 139 | 136, 138 | ifeq12d 4547 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 ·
(1r‘𝑅)),
(⦋𝑒 / 𝑖⦌𝑋 ·
(0g‘𝑅))) =
if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 140 | 133, 139 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 141 | 132, 140 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))) |
| 142 | 141 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))) |
| 143 | 142 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))) |
| 144 | 130, 143 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))) |
| 145 | 144 | ifeq1d 4545 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏))) |
| 146 | 145 | mpoeq3dva 7510 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))) |
| 147 | 146 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏))))) |
| 148 | 45, 35 | ring0cl 20264 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ 𝐾) |
| 149 | 65, 148 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (0g‘𝑅) ∈ 𝐾) |
| 150 | 149 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (0g‘𝑅) ∈ 𝐾) |
| 151 | 123, 150 | ifcld 4572 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) ∈ 𝐾) |
| 152 | 45, 134 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) |
| 153 | 65, 152 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (1r‘𝑅) ∈ 𝐾) |
| 154 | 153, 149 | ifcld 4572 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) |
| 155 | 45, 88 | ringcl 20247 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾) |
| 156 | 65, 99, 154, 155 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾) |
| 157 | 156 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾) |
| 158 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾) |
| 159 | 158 | fovcdmda 7604 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾) |
| 160 | 159 | 3impb 1115 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾) |
| 161 | 44, 45, 62, 63, 68, 151, 157, 160, 101 | mdetrlin2 22613 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))))) |
| 162 | 154 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) |
| 163 | 44, 45, 88, 63, 68, 162, 160, 99, 101 | mdetrsca2 22610 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 164 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀 ∈ 𝐵) |
| 165 | 48, 44, 78, 49, 134, 35 | maducoeval 22645 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 166 | 164, 96, 101, 165 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 167 | 166 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 168 | 163, 167 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) |
| 169 | 168 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))) |
| 170 | 147, 161,
169 | 3eqtrrd 2782 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 171 | 170 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 172 | 109, 111,
171 | 3eqtrd 2781 |
. . . 4
⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 173 | 172 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))) |
| 174 | 8, 16, 24, 32, 61, 173, 52 | findcard2d 9206 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) |
| 175 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑏(𝑋 · (𝑖(𝐽‘𝑀)𝐿)) |
| 176 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑖⦋𝑏 / 𝑖⦌𝑋 |
| 177 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑖
· |
| 178 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑖(𝑏(𝐽‘𝑀)𝐿) |
| 179 | 176, 177,
178 | nfov 7461 |
. . . 4
⊢
Ⅎ𝑖(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) |
| 180 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑖 = 𝑏 → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋) |
| 181 | | oveq1 7438 |
. . . . 5
⊢ (𝑖 = 𝑏 → (𝑖(𝐽‘𝑀)𝐿) = (𝑏(𝐽‘𝑀)𝐿)) |
| 182 | 180, 181 | oveq12d 7449 |
. . . 4
⊢ (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽‘𝑀)𝐿)) = (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) |
| 183 | 175, 179,
182 | cbvmpt 5253 |
. . 3
⊢ (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) |
| 184 | 183 | oveq2i 7442 |
. 2
⊢ (𝑅 Σg
(𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) |
| 185 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) |
| 186 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) |
| 187 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑗if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) |
| 188 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑖 𝑎 = 𝐿 |
| 189 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑖(𝑎𝑀𝑏) |
| 190 | 188, 176,
189 | nfif 4556 |
. . . . 5
⊢
Ⅎ𝑖if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) |
| 191 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑗 = 𝑎 → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿)) |
| 192 | 191 | adantr 480 |
. . . . . 6
⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿)) |
| 193 | 180 | adantl 481 |
. . . . . 6
⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋) |
| 194 | | oveq12 7440 |
. . . . . 6
⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏)) |
| 195 | 192, 193,
194 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) |
| 196 | 185, 186,
187, 190, 195 | cbvmpo 7527 |
. . . 4
⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) |
| 197 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝑁 → if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = ⦋𝑏 / 𝑖⦌𝑋) |
| 198 | 197 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑏 ∈ 𝑁 → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 199 | 198 | adantl 481 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) |
| 200 | 199 | ifeq1d 4545 |
. . . . 5
⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 201 | 200 | mpoeq3ia 7511 |
. . . 4
⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 202 | 196, 201 | eqtri 2765 |
. . 3
⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) |
| 203 | 202 | fveq2i 6909 |
. 2
⊢ (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) |
| 204 | 174, 184,
203 | 3eqtr4g 2802 |
1
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))))) |