Proof of Theorem baerlem5bmN
| Step | Hyp | Ref
| Expression |
| 1 | | baerlem3.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 2 | 1 | eldifad 3963 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 3 | | baerlem3.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
| 4 | 3 | eldifad 3963 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 5 | | baerlem3.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
| 6 | | baerlem5a.p |
. . . . . 6
⊢ + =
(+g‘𝑊) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝑊) = (invg‘𝑊) |
| 8 | | baerlem3.m |
. . . . . 6
⊢ − =
(-g‘𝑊) |
| 9 | 5, 6, 7, 8 | grpsubval 19003 |
. . . . 5
⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 − 𝑍) = (𝑌 +
((invg‘𝑊)‘𝑍))) |
| 10 | 2, 4, 9 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 +
((invg‘𝑊)‘𝑍))) |
| 11 | 10 | sneqd 4638 |
. . 3
⊢ (𝜑 → {(𝑌 − 𝑍)} = {(𝑌 +
((invg‘𝑊)‘𝑍))}) |
| 12 | 11 | fveq2d 6910 |
. 2
⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (𝑁‘{(𝑌 +
((invg‘𝑊)‘𝑍))})) |
| 13 | | baerlem3.o |
. . 3
⊢ 0 =
(0g‘𝑊) |
| 14 | | baerlem3.s |
. . 3
⊢ ⊕ =
(LSSum‘𝑊) |
| 15 | | baerlem3.n |
. . 3
⊢ 𝑁 = (LSpan‘𝑊) |
| 16 | | baerlem3.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 17 | | baerlem3.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 18 | | lveclmod 21105 |
. . . . . 6
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 19 | 16, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 20 | 5, 7 | lmodvnegcl 20901 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → ((invg‘𝑊)‘𝑍) ∈ 𝑉) |
| 21 | 19, 4, 20 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
((invg‘𝑊)‘𝑍) ∈ 𝑉) |
| 22 | | eqid 2737 |
. . . . . 6
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 23 | 5, 22, 15, 19, 2, 4 | lspprcl 20976 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊)) |
| 24 | | baerlem3.c |
. . . . . 6
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
| 25 | 13, 22, 19, 23, 17, 24 | lssneln0 20951 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
| 26 | 5, 15, 16, 17, 2, 4, 24 | lspindpi 21134 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))) |
| 27 | 26 | simpld 494 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
| 28 | 5, 13, 15, 16, 25, 2, 27 | lspsnne1 21119 |
. . . 4
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) |
| 29 | | baerlem3.d |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
| 30 | 29 | necomd 2996 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌})) |
| 31 | 5, 13, 15, 16, 3, 2, 30 | lspsnne1 21119 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑌})) |
| 32 | 5, 15, 16, 17, 4, 2, 31, 24 | lspexchn2 21133 |
. . . . 5
⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑌, 𝑋})) |
| 33 | | lmodgrp 20865 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 34 | 19, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Grp) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑊 ∈ Grp) |
| 36 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑍 ∈ 𝑉) |
| 37 | 5, 7 | grpinvinv 19023 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑍 ∈ 𝑉) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) = 𝑍) |
| 38 | 35, 36, 37 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) = 𝑍) |
| 39 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑊 ∈ LMod) |
| 40 | 5, 22, 15, 19, 2, 17 | lspprcl 20976 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊)) |
| 41 | 40 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊)) |
| 42 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) |
| 43 | 22, 7 | lssvnegcl 20954 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊) ∧ ((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) ∈ (𝑁‘{𝑌, 𝑋})) |
| 44 | 39, 41, 42, 43 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) ∈ (𝑁‘{𝑌, 𝑋})) |
| 45 | 38, 44 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑍 ∈ (𝑁‘{𝑌, 𝑋})) |
| 46 | 32, 45 | mtand 816 |
. . . 4
⊢ (𝜑 → ¬
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) |
| 47 | 5, 15, 16, 21, 17, 2, 28, 46 | lspexchn2 21133 |
. . 3
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, ((invg‘𝑊)‘𝑍)})) |
| 48 | 5, 7, 15 | lspsnneg 21004 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{((invg‘𝑊)‘𝑍)}) = (𝑁‘{𝑍})) |
| 49 | 19, 4, 48 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑁‘{((invg‘𝑊)‘𝑍)}) = (𝑁‘{𝑍})) |
| 50 | 29, 49 | neeqtrrd 3015 |
. . 3
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{((invg‘𝑊)‘𝑍)})) |
| 51 | 5, 13, 7 | grpinvnzcl 19029 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑍 ∈ (𝑉 ∖ { 0 })) →
((invg‘𝑊)‘𝑍) ∈ (𝑉 ∖ { 0 })) |
| 52 | 34, 3, 51 | syl2anc 584 |
. . 3
⊢ (𝜑 →
((invg‘𝑊)‘𝑍) ∈ (𝑉 ∖ { 0 })) |
| 53 | 5, 8, 13, 14, 15, 16, 17, 47, 50, 1, 52, 6 | baerlem5b 41717 |
. 2
⊢ (𝜑 → (𝑁‘{(𝑌 +
((invg‘𝑊)‘𝑍))}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) ∩ ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋})))) |
| 54 | 49 | oveq2d 7447 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) = ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍}))) |
| 55 | 10 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → (𝑌 +
((invg‘𝑊)‘𝑍)) = (𝑌 − 𝑍)) |
| 56 | 55 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍))) = (𝑋 − (𝑌 − 𝑍))) |
| 57 | 56 | sneqd 4638 |
. . . . 5
⊢ (𝜑 → {(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))} = {(𝑋 − (𝑌 − 𝑍))}) |
| 58 | 57 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) = (𝑁‘{(𝑋 − (𝑌 − 𝑍))})) |
| 59 | 58 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋})) = ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋}))) |
| 60 | 54, 59 | ineq12d 4221 |
. 2
⊢ (𝜑 → (((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) ∩ ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋}))) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) |
| 61 | 12, 53, 60 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) |