Proof of Theorem baerlem5bmN
Step | Hyp | Ref
| Expression |
1 | | baerlem3.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
2 | 1 | eldifad 3586 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
3 | | baerlem3.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) |
4 | 3 | eldifad 3586 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
5 | | baerlem3.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑊) |
6 | | baerlem5a.p |
. . . . . 6
⊢ + =
(+g‘𝑊) |
7 | | eqid 2622 |
. . . . . 6
⊢
(invg‘𝑊) = (invg‘𝑊) |
8 | | baerlem3.m |
. . . . . 6
⊢ − =
(-g‘𝑊) |
9 | 5, 6, 7, 8 | grpsubval 17465 |
. . . . 5
⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 − 𝑍) = (𝑌 +
((invg‘𝑊)‘𝑍))) |
10 | 2, 4, 9 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 +
((invg‘𝑊)‘𝑍))) |
11 | 10 | sneqd 4189 |
. . 3
⊢ (𝜑 → {(𝑌 − 𝑍)} = {(𝑌 +
((invg‘𝑊)‘𝑍))}) |
12 | 11 | fveq2d 6195 |
. 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 19106 |
. . . . . 6
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
19 | 16, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
20 | 5, 7 | lmodvnegcl 18904 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → ((invg‘𝑊)‘𝑍) ∈ 𝑉) |
21 | 19, 4, 20 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
((invg‘𝑊)‘𝑍) ∈ 𝑉) |
22 | | eqid 2622 |
. . . . . 6
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
23 | 5, 22, 15, 19, 2, 4 | lspprcl 18978 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) ∈ (LSubSp‘𝑊)) |
24 | | baerlem3.c |
. . . . . 6
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) |
25 | 5, 13, 22, 19, 23, 17, 24 | lssneln0 18952 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
26 | 5, 15, 16, 17, 2, 4, 24 | lspindpi 19132 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))) |
27 | 26 | simpld 475 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
28 | 5, 13, 15, 16, 25, 2, 27 | lspsnne1 19117 |
. . . 4
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌})) |
29 | | baerlem3.d |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍})) |
30 | 29 | necomd 2849 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{𝑌})) |
31 | 5, 13, 15, 16, 3, 2, 30 | lspsnne1 19117 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑌})) |
32 | 5, 15, 16, 17, 4, 2, 31, 24 | lspexchn2 19131 |
. . . . 5
⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑌, 𝑋})) |
33 | | lmodgrp 18870 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
34 | 19, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Grp) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑊 ∈ Grp) |
36 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑍 ∈ 𝑉) |
37 | 5, 7 | grpinvinv 17482 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑍 ∈ 𝑉) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) = 𝑍) |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) = 𝑍) |
39 | 19 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑊 ∈ LMod) |
40 | 5, 22, 15, 19, 2, 17 | lspprcl 18978 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊)) |
41 | 40 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊)) |
42 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) |
43 | 22, 7 | lssvnegcl 18956 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑌, 𝑋}) ∈ (LSubSp‘𝑊) ∧ ((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) ∈ (𝑁‘{𝑌, 𝑋})) |
44 | 39, 41, 42, 43 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → ((invg‘𝑊)‘((invg‘𝑊)‘𝑍)) ∈ (𝑁‘{𝑌, 𝑋})) |
45 | 38, 44 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝜑 ∧
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) → 𝑍 ∈ (𝑁‘{𝑌, 𝑋})) |
46 | 32, 45 | mtand 691 |
. . . 4
⊢ (𝜑 → ¬
((invg‘𝑊)‘𝑍) ∈ (𝑁‘{𝑌, 𝑋})) |
47 | 5, 15, 16, 21, 17, 2, 28, 46 | lspexchn2 19131 |
. . 3
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, ((invg‘𝑊)‘𝑍)})) |
48 | 5, 7, 15 | lspsnneg 19006 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{((invg‘𝑊)‘𝑍)}) = (𝑁‘{𝑍})) |
49 | 19, 4, 48 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑁‘{((invg‘𝑊)‘𝑍)}) = (𝑁‘{𝑍})) |
50 | 29, 49 | neeqtrrd 2868 |
. . 3
⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{((invg‘𝑊)‘𝑍)})) |
51 | 5, 13, 7 | grpinvnzcl 17487 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑍 ∈ (𝑉 ∖ { 0 })) →
((invg‘𝑊)‘𝑍) ∈ (𝑉 ∖ { 0 })) |
52 | 34, 3, 51 | syl2anc 693 |
. . 3
⊢ (𝜑 →
((invg‘𝑊)‘𝑍) ∈ (𝑉 ∖ { 0 })) |
53 | 5, 8, 13, 14, 15, 16, 17, 47, 50, 1, 52, 6 | baerlem5b 37004 |
. 2
⊢ (𝜑 → (𝑁‘{(𝑌 +
((invg‘𝑊)‘𝑍))}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) ∩ ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋})))) |
54 | 49 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) = ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍}))) |
55 | 10 | eqcomd 2628 |
. . . . . . 7
⊢ (𝜑 → (𝑌 +
((invg‘𝑊)‘𝑍)) = (𝑌 − 𝑍)) |
56 | 55 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍))) = (𝑋 − (𝑌 − 𝑍))) |
57 | 56 | sneqd 4189 |
. . . . 5
⊢ (𝜑 → {(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))} = {(𝑋 − (𝑌 − 𝑍))}) |
58 | 57 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) = (𝑁‘{(𝑋 − (𝑌 − 𝑍))})) |
59 | 58 | oveq1d 6665 |
. . 3
⊢ (𝜑 → ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋})) = ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋}))) |
60 | 54, 59 | ineq12d 3815 |
. 2
⊢ (𝜑 → (((𝑁‘{𝑌}) ⊕ (𝑁‘{((invg‘𝑊)‘𝑍)})) ∩ ((𝑁‘{(𝑋 − (𝑌 +
((invg‘𝑊)‘𝑍)))}) ⊕ (𝑁‘{𝑋}))) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) |
61 | 12, 53, 60 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − (𝑌 − 𝑍))}) ⊕ (𝑁‘{𝑋})))) |