Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | | lshpcmp.h |
. . . . 5
⊢ 𝐻 = (LSHyp‘𝑊) |
3 | | lshpcmp.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LVec) |
4 | | lveclmod 20143 |
. . . . . 6
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
6 | | lshpcmp.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐻) |
7 | 1, 2, 5, 6 | lshpne 36733 |
. . . 4
⊢ (𝜑 → 𝑈 ≠ (Base‘𝑊)) |
8 | | eqid 2737 |
. . . . . . . 8
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
9 | 8, 2, 5, 6 | lshplss 36732 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊)) |
10 | 1, 8 | lssss 19973 |
. . . . . . 7
⊢ (𝑈 ∈ (LSubSp‘𝑊) → 𝑈 ⊆ (Base‘𝑊)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑊)) |
12 | | lshpcmp.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐻) |
13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
14 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
15 | 1, 13, 8, 14, 2, 5 | islshpsm 36731 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ (LSubSp‘𝑊) ∧ 𝑇 ≠ (Base‘𝑊) ∧ ∃𝑣 ∈ (Base‘𝑊)(𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊)))) |
16 | 12, 15 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∈ (LSubSp‘𝑊) ∧ 𝑇 ≠ (Base‘𝑊) ∧ ∃𝑣 ∈ (Base‘𝑊)(𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) |
17 | 16 | simp3d 1146 |
. . . . . . 7
⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑊)(𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊)) |
18 | | id 22 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) → (𝜑 ∧ 𝑣 ∈ (Base‘𝑊))) |
19 | 18 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) → (𝜑 ∧ 𝑣 ∈ (Base‘𝑊))) |
20 | 3 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑊 ∈ LVec) |
21 | 8, 2, 5, 12 | lshplss 36732 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑊)) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑇 ∈ (LSubSp‘𝑊)) |
23 | 9 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑈 ∈ (LSubSp‘𝑊)) |
24 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) → 𝑣 ∈ (Base‘𝑊)) |
25 | 1, 8, 13, 14, 20, 22, 23, 24 | lsmcv 20178 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣}))) → 𝑈 = (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣}))) |
26 | 19, 25 | syl3an1 1165 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣}))) → 𝑈 = (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣}))) |
27 | 26 | 3expia 1123 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈) → (𝑈 ⊆ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) → 𝑈 = (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})))) |
28 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈) → (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊)) |
29 | 28 | sseq2d 3933 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈) → (𝑈 ⊆ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) ↔ 𝑈 ⊆ (Base‘𝑊))) |
30 | 28 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈) → (𝑈 = (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) ↔ 𝑈 = (Base‘𝑊))) |
31 | 27, 29, 30 | 3imtr3d 296 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ (𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊))) ∧ 𝑇 ⊊ 𝑈) → (𝑈 ⊆ (Base‘𝑊) → 𝑈 = (Base‘𝑊))) |
32 | 31 | exp42 439 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ (Base‘𝑊) → ((𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊) → (𝑇 ⊊ 𝑈 → (𝑈 ⊆ (Base‘𝑊) → 𝑈 = (Base‘𝑊)))))) |
33 | 32 | rexlimdv 3202 |
. . . . . . 7
⊢ (𝜑 → (∃𝑣 ∈ (Base‘𝑊)(𝑇(LSSum‘𝑊)((LSpan‘𝑊)‘{𝑣})) = (Base‘𝑊) → (𝑇 ⊊ 𝑈 → (𝑈 ⊆ (Base‘𝑊) → 𝑈 = (Base‘𝑊))))) |
34 | 17, 33 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝑇 ⊊ 𝑈 → (𝑈 ⊆ (Base‘𝑊) → 𝑈 = (Base‘𝑊)))) |
35 | 11, 34 | mpid 44 |
. . . . 5
⊢ (𝜑 → (𝑇 ⊊ 𝑈 → 𝑈 = (Base‘𝑊))) |
36 | 35 | necon3ad 2953 |
. . . 4
⊢ (𝜑 → (𝑈 ≠ (Base‘𝑊) → ¬ 𝑇 ⊊ 𝑈)) |
37 | 7, 36 | mpd 15 |
. . 3
⊢ (𝜑 → ¬ 𝑇 ⊊ 𝑈) |
38 | | df-pss 3885 |
. . . . 5
⊢ (𝑇 ⊊ 𝑈 ↔ (𝑇 ⊆ 𝑈 ∧ 𝑇 ≠ 𝑈)) |
39 | 38 | simplbi2 504 |
. . . 4
⊢ (𝑇 ⊆ 𝑈 → (𝑇 ≠ 𝑈 → 𝑇 ⊊ 𝑈)) |
40 | 39 | necon1bd 2958 |
. . 3
⊢ (𝑇 ⊆ 𝑈 → (¬ 𝑇 ⊊ 𝑈 → 𝑇 = 𝑈)) |
41 | 37, 40 | syl5com 31 |
. 2
⊢ (𝜑 → (𝑇 ⊆ 𝑈 → 𝑇 = 𝑈)) |
42 | | eqimss 3957 |
. 2
⊢ (𝑇 = 𝑈 → 𝑇 ⊆ 𝑈) |
43 | 41, 42 | impbid1 228 |
1
⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) |