Proof of Theorem mdetunilem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdetunilem2.ph | . 2
⊢ (𝜓 → 𝜑) | 
| 2 |  | mdetuni.a | . . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 3 |  | mdetuni.k | . . 3
⊢ 𝐾 = (Base‘𝑅) | 
| 4 |  | mdetuni.b | . . 3
⊢ 𝐵 = (Base‘𝐴) | 
| 5 |  | mdetuni.n | . . . 4
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 6 | 1, 5 | syl 17 | . . 3
⊢ (𝜓 → 𝑁 ∈ Fin) | 
| 7 |  | mdetuni.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 8 | 1, 7 | syl 17 | . . 3
⊢ (𝜓 → 𝑅 ∈ Ring) | 
| 9 |  | mdetunilem2.f | . . . . 5
⊢ ((𝜓 ∧ 𝑏 ∈ 𝑁) → 𝐹 ∈ 𝐾) | 
| 10 | 9 | 3adant2 1132 | . . . 4
⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐹 ∈ 𝐾) | 
| 11 |  | mdetunilem2.h | . . . . 5
⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐻 ∈ 𝐾) | 
| 12 | 10, 11 | ifcld 4572 | . . . 4
⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐺, 𝐹, 𝐻) ∈ 𝐾) | 
| 13 | 10, 12 | ifcld 4572 | . . 3
⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) ∈ 𝐾) | 
| 14 | 2, 3, 4, 6, 8, 13 | matbas2d 22429 | . 2
⊢ (𝜓 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) ∈ 𝐵) | 
| 15 |  | eqidd 2738 | . . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) | 
| 16 |  | iftrue 4531 | . . . . . . 7
⊢ (𝑎 = 𝐸 → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = 𝐹) | 
| 17 |  | csbeq1a 3913 | . . . . . . 7
⊢ (𝑏 = 𝑤 → 𝐹 = ⦋𝑤 / 𝑏⦌𝐹) | 
| 18 | 16, 17 | sylan9eq 2797 | . . . . . 6
⊢ ((𝑎 = 𝐸 ∧ 𝑏 = 𝑤) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 19 | 18 | adantl 481 | . . . . 5
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ (𝑎 = 𝐸 ∧ 𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 20 |  | eqidd 2738 | . . . . 5
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ 𝑎 = 𝐸) → 𝑁 = 𝑁) | 
| 21 |  | mdetunilem2.eg | . . . . . . 7
⊢ (𝜓 → (𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺)) | 
| 22 | 21 | simp1d 1143 | . . . . . 6
⊢ (𝜓 → 𝐸 ∈ 𝑁) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → 𝐸 ∈ 𝑁) | 
| 24 |  | simpr 484 | . . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → 𝑤 ∈ 𝑁) | 
| 25 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑏(𝜓 ∧ 𝑤 ∈ 𝑁) | 
| 26 |  | nfcsb1v 3923 | . . . . . . . 8
⊢
Ⅎ𝑏⦋𝑤 / 𝑏⦌𝐹 | 
| 27 | 26 | nfel1 2922 | . . . . . . 7
⊢
Ⅎ𝑏⦋𝑤 / 𝑏⦌𝐹 ∈ 𝐾 | 
| 28 | 25, 27 | nfim 1896 | . . . . . 6
⊢
Ⅎ𝑏((𝜓 ∧ 𝑤 ∈ 𝑁) → ⦋𝑤 / 𝑏⦌𝐹 ∈ 𝐾) | 
| 29 |  | eleq1w 2824 | . . . . . . . 8
⊢ (𝑏 = 𝑤 → (𝑏 ∈ 𝑁 ↔ 𝑤 ∈ 𝑁)) | 
| 30 | 29 | anbi2d 630 | . . . . . . 7
⊢ (𝑏 = 𝑤 → ((𝜓 ∧ 𝑏 ∈ 𝑁) ↔ (𝜓 ∧ 𝑤 ∈ 𝑁))) | 
| 31 | 17 | eleq1d 2826 | . . . . . . 7
⊢ (𝑏 = 𝑤 → (𝐹 ∈ 𝐾 ↔ ⦋𝑤 / 𝑏⦌𝐹 ∈ 𝐾)) | 
| 32 | 30, 31 | imbi12d 344 | . . . . . 6
⊢ (𝑏 = 𝑤 → (((𝜓 ∧ 𝑏 ∈ 𝑁) → 𝐹 ∈ 𝐾) ↔ ((𝜓 ∧ 𝑤 ∈ 𝑁) → ⦋𝑤 / 𝑏⦌𝐹 ∈ 𝐾))) | 
| 33 | 28, 32, 9 | chvarfv 2240 | . . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → ⦋𝑤 / 𝑏⦌𝐹 ∈ 𝐾) | 
| 34 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑎(𝜓 ∧ 𝑤 ∈ 𝑁) | 
| 35 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑏𝐸 | 
| 36 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑎𝑤 | 
| 37 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑎⦋𝑤 / 𝑏⦌𝐹 | 
| 38 | 15, 19, 20, 23, 24, 33, 34, 25, 35, 36, 37, 26 | ovmpodxf 7583 | . . . 4
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → (𝐸(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 39 | 21 | simp3d 1145 | . . . . . . . . . . . . 13
⊢ (𝜓 → 𝐸 ≠ 𝐺) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → 𝐸 ≠ 𝐺) | 
| 41 |  | neeq2 3004 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝐺 → (𝐸 ≠ 𝑎 ↔ 𝐸 ≠ 𝐺)) | 
| 42 | 40, 41 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → (𝑎 = 𝐺 → 𝐸 ≠ 𝑎)) | 
| 43 | 42 | imp 406 | . . . . . . . . . 10
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ 𝑎 = 𝐺) → 𝐸 ≠ 𝑎) | 
| 44 | 43 | necomd 2996 | . . . . . . . . 9
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ 𝑎 = 𝐺) → 𝑎 ≠ 𝐸) | 
| 45 | 44 | neneqd 2945 | . . . . . . . 8
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ 𝑎 = 𝐺) → ¬ 𝑎 = 𝐸) | 
| 46 | 45 | adantrr 717 | . . . . . . 7
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ (𝑎 = 𝐺 ∧ 𝑏 = 𝑤)) → ¬ 𝑎 = 𝐸) | 
| 47 | 46 | iffalsed 4536 | . . . . . 6
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ (𝑎 = 𝐺 ∧ 𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = if(𝑎 = 𝐺, 𝐹, 𝐻)) | 
| 48 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑎 = 𝐺 → if(𝑎 = 𝐺, 𝐹, 𝐻) = 𝐹) | 
| 49 | 48, 17 | sylan9eq 2797 | . . . . . . 7
⊢ ((𝑎 = 𝐺 ∧ 𝑏 = 𝑤) → if(𝑎 = 𝐺, 𝐹, 𝐻) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 50 | 49 | adantl 481 | . . . . . 6
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ (𝑎 = 𝐺 ∧ 𝑏 = 𝑤)) → if(𝑎 = 𝐺, 𝐹, 𝐻) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 51 | 47, 50 | eqtrd 2777 | . . . . 5
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ (𝑎 = 𝐺 ∧ 𝑏 = 𝑤)) → if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 52 |  | eqidd 2738 | . . . . 5
⊢ (((𝜓 ∧ 𝑤 ∈ 𝑁) ∧ 𝑎 = 𝐺) → 𝑁 = 𝑁) | 
| 53 | 21 | simp2d 1144 | . . . . . 6
⊢ (𝜓 → 𝐺 ∈ 𝑁) | 
| 54 | 53 | adantr 480 | . . . . 5
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → 𝐺 ∈ 𝑁) | 
| 55 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑏𝐺 | 
| 56 | 15, 51, 52, 54, 24, 33, 34, 25, 55, 36, 37, 26 | ovmpodxf 7583 | . . . 4
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → (𝐺(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = ⦋𝑤 / 𝑏⦌𝐹) | 
| 57 | 38, 56 | eqtr4d 2780 | . . 3
⊢ ((𝜓 ∧ 𝑤 ∈ 𝑁) → (𝐸(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤)) | 
| 58 | 57 | ralrimiva 3146 | . 2
⊢ (𝜓 → ∀𝑤 ∈ 𝑁 (𝐸(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤)) | 
| 59 |  | mdetuni.0g | . . 3
⊢  0 =
(0g‘𝑅) | 
| 60 |  | mdetuni.1r | . . 3
⊢  1 =
(1r‘𝑅) | 
| 61 |  | mdetuni.pg | . . 3
⊢  + =
(+g‘𝑅) | 
| 62 |  | mdetuni.tg | . . 3
⊢  · =
(.r‘𝑅) | 
| 63 |  | mdetuni.ff | . . 3
⊢ (𝜑 → 𝐷:𝐵⟶𝐾) | 
| 64 |  | mdetuni.al | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) | 
| 65 |  | mdetuni.li | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) | 
| 66 |  | mdetuni.sc | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) | 
| 67 | 2, 4, 3, 59, 60, 61, 62, 5, 7, 63, 64, 65, 66 | mdetunilem1 22618 | . 2
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻))) ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐸(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤) = (𝐺(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))𝑤)) ∧ (𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺)) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 ) | 
| 68 | 1, 14, 58, 21, 67 | syl31anc 1375 | 1
⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 ) |