Proof of Theorem mdetrlin2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdetrlin2.d | . 2
⊢ 𝐷 = (𝑁 maDet 𝑅) | 
| 2 |  | eqid 2736 | . 2
⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅) | 
| 3 |  | eqid 2736 | . 2
⊢
(Base‘(𝑁 Mat
𝑅)) = (Base‘(𝑁 Mat 𝑅)) | 
| 4 |  | mdetrlin2.p | . 2
⊢  + =
(+g‘𝑅) | 
| 5 |  | mdetrlin2.r | . 2
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 6 |  | mdetrlin2.k | . . 3
⊢ 𝐾 = (Base‘𝑅) | 
| 7 |  | mdetrlin2.n | . . 3
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 8 |  | crngring 20243 | . . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 9 | 5, 8 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 10 | 9 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) | 
| 11 |  | mdetrlin2.x | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) | 
| 12 |  | mdetrlin2.y | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) | 
| 13 | 6, 4 | ringacl 20276 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | 
| 14 | 10, 11, 12, 13 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑋 + 𝑌) ∈ 𝐾) | 
| 15 |  | mdetrlin2.z | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾) | 
| 16 | 14, 15 | ifcld 4571 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) ∈ 𝐾) | 
| 17 | 2, 6, 3, 7, 5, 16 | matbas2d 22430 | . 2
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ∈ (Base‘(𝑁 Mat 𝑅))) | 
| 18 | 11, 15 | ifcld 4571 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, 𝑋, 𝑍) ∈ 𝐾) | 
| 19 | 2, 6, 3, 7, 5, 18 | matbas2d 22430 | . 2
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ∈ (Base‘(𝑁 Mat 𝑅))) | 
| 20 | 12, 15 | ifcld 4571 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, 𝑌, 𝑍) ∈ 𝐾) | 
| 21 | 2, 6, 3, 7, 5, 20 | matbas2d 22430 | . 2
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ∈ (Base‘(𝑁 Mat 𝑅))) | 
| 22 |  | mdetrlin2.i | . 2
⊢ (𝜑 → 𝐼 ∈ 𝑁) | 
| 23 |  | snex 5435 | . . . . . . 7
⊢ {𝐼} ∈ V | 
| 24 | 23 | a1i 11 | . . . . . 6
⊢ (𝜑 → {𝐼} ∈ V) | 
| 25 | 22 | snssd 4808 | . . . . . . . . 9
⊢ (𝜑 → {𝐼} ⊆ 𝑁) | 
| 26 | 25 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ {𝐼} ∧ 𝑗 ∈ 𝑁) → {𝐼} ⊆ 𝑁) | 
| 27 |  | simp2 1137 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ {𝐼} ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ {𝐼}) | 
| 28 | 26, 27 | sseldd 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ {𝐼} ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) | 
| 29 | 28, 11 | syld3an2 1412 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ {𝐼} ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) | 
| 30 | 28, 12 | syld3an2 1412 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ {𝐼} ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) | 
| 31 |  | eqidd 2737 | . . . . . 6
⊢ (𝜑 → (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋)) | 
| 32 |  | eqidd 2737 | . . . . . 6
⊢ (𝜑 → (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌)) | 
| 33 | 24, 7, 29, 30, 31, 32 | offval22 8114 | . . . . 5
⊢ (𝜑 → ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ (𝑋 + 𝑌))) | 
| 34 | 33 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ (𝑋 + 𝑌)) = ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌))) | 
| 35 |  | mposnif 7550 | . . . 4
⊢ (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ (𝑋 + 𝑌)) | 
| 36 |  | mposnif 7550 | . . . . 5
⊢ (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋) | 
| 37 |  | mposnif 7550 | . . . . 5
⊢ (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌) | 
| 38 | 36, 37 | oveq12i 7444 | . . . 4
⊢ ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))) = ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑋) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ 𝑌)) | 
| 39 | 34, 35, 38 | 3eqtr4g 2801 | . . 3
⊢ (𝜑 → (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) = ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)))) | 
| 40 |  | ssid 4005 | . . . 4
⊢ 𝑁 ⊆ 𝑁 | 
| 41 |  | resmpo 7554 | . . . 4
⊢ (({𝐼} ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) | 
| 42 | 25, 40, 41 | sylancl 586 | . . 3
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) | 
| 43 |  | resmpo 7554 | . . . . 5
⊢ (({𝐼} ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) | 
| 44 | 25, 40, 43 | sylancl 586 | . . . 4
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) | 
| 45 |  | resmpo 7554 | . . . . 5
⊢ (({𝐼} ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))) | 
| 46 | 25, 40, 45 | sylancl 586 | . . . 4
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ({𝐼} × 𝑁)) = (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))) | 
| 47 | 44, 46 | oveq12d 7450 | . . 3
⊢ (𝜑 → (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ({𝐼} × 𝑁)) ∘f + ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ({𝐼} × 𝑁))) = ((𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ∘f + (𝑖 ∈ {𝐼}, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)))) | 
| 48 | 39, 42, 47 | 3eqtr4d 2786 | . 2
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ({𝐼} × 𝑁)) = (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ({𝐼} × 𝑁)) ∘f + ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ({𝐼} × 𝑁)))) | 
| 49 |  | eldifsni 4789 | . . . . . . 7
⊢ (𝑖 ∈ (𝑁 ∖ {𝐼}) → 𝑖 ≠ 𝐼) | 
| 50 | 49 | neneqd 2944 | . . . . . 6
⊢ (𝑖 ∈ (𝑁 ∖ {𝐼}) → ¬ 𝑖 = 𝐼) | 
| 51 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
𝑖 = 𝐼 → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = 𝑍) | 
| 52 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
𝑖 = 𝐼 → if(𝑖 = 𝐼, 𝑋, 𝑍) = 𝑍) | 
| 53 | 51, 52 | eqtr4d 2779 | . . . . . 6
⊢ (¬
𝑖 = 𝐼 → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑋, 𝑍)) | 
| 54 | 50, 53 | syl 17 | . . . . 5
⊢ (𝑖 ∈ (𝑁 ∖ {𝐼}) → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑋, 𝑍)) | 
| 55 | 54 | 3ad2ant2 1134 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁 ∖ {𝐼}) ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑋, 𝑍)) | 
| 56 | 55 | mpoeq3dva 7511 | . . 3
⊢ (𝜑 → (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) | 
| 57 |  | difss 4135 | . . . 4
⊢ (𝑁 ∖ {𝐼}) ⊆ 𝑁 | 
| 58 |  | resmpo 7554 | . . . 4
⊢ (((𝑁 ∖ {𝐼}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) | 
| 59 | 57, 40, 58 | mp2an 692 | . . 3
⊢ ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) | 
| 60 |  | resmpo 7554 | . . . 4
⊢ (((𝑁 ∖ {𝐼}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) | 
| 61 | 57, 40, 60 | mp2an 692 | . . 3
⊢ ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) | 
| 62 | 56, 59, 61 | 3eqtr4g 2801 | . 2
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) | 
| 63 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
𝑖 = 𝐼 → if(𝑖 = 𝐼, 𝑌, 𝑍) = 𝑍) | 
| 64 | 51, 63 | eqtr4d 2779 | . . . . . 6
⊢ (¬
𝑖 = 𝐼 → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑌, 𝑍)) | 
| 65 | 50, 64 | syl 17 | . . . . 5
⊢ (𝑖 ∈ (𝑁 ∖ {𝐼}) → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑌, 𝑍)) | 
| 66 | 65 | 3ad2ant2 1134 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁 ∖ {𝐼}) ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍) = if(𝑖 = 𝐼, 𝑌, 𝑍)) | 
| 67 | 66 | mpoeq3dva 7511 | . . 3
⊢ (𝜑 → (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))) | 
| 68 |  | resmpo 7554 | . . . 4
⊢ (((𝑁 ∖ {𝐼}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))) | 
| 69 | 57, 40, 68 | mp2an 692 | . . 3
⊢ ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐼}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) | 
| 70 | 67, 59, 69 | 3eqtr4g 2801 | . 2
⊢ (𝜑 → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)) ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) | 
| 71 | 1, 2, 3, 4, 5, 17,
19, 21, 22, 48, 62, 70 | mdetrlin 22609 | 1
⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) = ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) + (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))))) |