| Step | Hyp | Ref
| Expression |
| 1 | | lshpnelb.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ 𝐻) |
| 2 | | lshpnelb.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
| 3 | | lshpnelb.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑊) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 5 | | lshpnelb.p |
. . . . . . 7
⊢ ⊕ =
(LSSum‘𝑊) |
| 6 | | lshpnelb.h |
. . . . . . 7
⊢ 𝐻 = (LSHyp‘𝑊) |
| 7 | | lshpnelb.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 8 | | lveclmod 21105 |
. . . . . . . 8
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 10 | 2, 3, 4, 5, 6, 9 | islshpsm 38981 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉))) |
| 11 | 1, 10 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉)) |
| 12 | 11 | simp3d 1145 |
. . . 4
⊢ (𝜑 → ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) |
| 14 | | simp1l 1198 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → 𝜑) |
| 15 | | simp2 1138 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → 𝑣 ∈ 𝑉) |
| 16 | 4 | lsssssubg 20956 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ LMod →
(LSubSp‘𝑊) ⊆
(SubGrp‘𝑊)) |
| 17 | 9, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊)) |
| 18 | 4, 6, 9, 1 | lshplss 38982 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊)) |
| 19 | 17, 18 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑊)) |
| 20 | | lshpnelb.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 21 | 2, 4, 3 | lspsncl 20975 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
| 22 | 9, 20, 21 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) |
| 23 | 17, 22 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) |
| 24 | 5 | lsmub1 19675 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) → 𝑈 ⊆ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 25 | 19, 23, 24 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → 𝑈 ⊆ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 27 | 5 | lsmub2 19676 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (SubGrp‘𝑊)) → (𝑁‘{𝑋}) ⊆ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 28 | 19, 23, 27 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 29 | 2, 3 | lspsnid 20991 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝑁‘{𝑋})) |
| 30 | 9, 20, 29 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋})) |
| 31 | 28, 30 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 32 | | nelne1 3039 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (𝑈 ⊕ (𝑁‘{𝑋})) ∧ ¬ 𝑋 ∈ 𝑈) → (𝑈 ⊕ (𝑁‘{𝑋})) ≠ 𝑈) |
| 33 | 31, 32 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → (𝑈 ⊕ (𝑁‘{𝑋})) ≠ 𝑈) |
| 34 | 33 | necomd 2996 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → 𝑈 ≠ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 35 | | df-pss 3971 |
. . . . . . . 8
⊢ (𝑈 ⊊ (𝑈 ⊕ (𝑁‘{𝑋})) ↔ (𝑈 ⊆ (𝑈 ⊕ (𝑁‘{𝑋})) ∧ 𝑈 ≠ (𝑈 ⊕ (𝑁‘{𝑋})))) |
| 36 | 26, 34, 35 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → 𝑈 ⊊ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → 𝑈 ⊊ (𝑈 ⊕ (𝑁‘{𝑋}))) |
| 38 | 4, 5 | lsmcl 21082 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊) ∧ (𝑁‘{𝑋}) ∈ (LSubSp‘𝑊)) → (𝑈 ⊕ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) |
| 39 | 9, 18, 22, 38 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) |
| 40 | 2, 4 | lssss 20934 |
. . . . . . . . . . 11
⊢ ((𝑈 ⊕ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊) → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ 𝑉) |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ 𝑉) |
| 42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ 𝑉) |
| 43 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) |
| 44 | 42, 43 | sseqtrrd 4021 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ (𝑈 ⊕ (𝑁‘{𝑣}))) |
| 45 | 44 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ (𝑈 ⊕ (𝑁‘{𝑣}))) |
| 46 | 45 | 3adant2 1132 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ (𝑈 ⊕ (𝑁‘{𝑣}))) |
| 47 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ LVec) |
| 48 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (LSubSp‘𝑊)) |
| 49 | 39 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) ∈ (LSubSp‘𝑊)) |
| 50 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
| 51 | 2, 4, 3, 5, 47, 48, 49, 50 | lsmcv 21143 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑈 ⊊ (𝑈 ⊕ (𝑁‘{𝑋})) ∧ (𝑈 ⊕ (𝑁‘{𝑋})) ⊆ (𝑈 ⊕ (𝑁‘{𝑣}))) → (𝑈 ⊕ (𝑁‘{𝑋})) = (𝑈 ⊕ (𝑁‘{𝑣}))) |
| 52 | 14, 15, 37, 46, 51 | syl211anc 1378 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) = (𝑈 ⊕ (𝑁‘{𝑣}))) |
| 53 | | simp3 1139 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) |
| 54 | 52, 53 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) ∧ 𝑣 ∈ 𝑉 ∧ (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) |
| 55 | 54 | rexlimdv3a 3159 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → (∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉 → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)) |
| 56 | 13, 55 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 ∈ 𝑈) → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) |
| 57 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) → 𝑊 ∈ LMod) |
| 58 | 1 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) → 𝑈 ∈ 𝐻) |
| 59 | 20 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) → 𝑋 ∈ 𝑉) |
| 60 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) → (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) |
| 61 | 2, 3, 5, 6, 57, 58, 59, 60 | lshpnel 38984 |
. 2
⊢ ((𝜑 ∧ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉) → ¬ 𝑋 ∈ 𝑈) |
| 62 | 56, 61 | impbida 801 |
1
⊢ (𝜑 → (¬ 𝑋 ∈ 𝑈 ↔ (𝑈 ⊕ (𝑁‘{𝑋})) = 𝑉)) |