Step | Hyp | Ref
| Expression |
1 | | lsatcmp.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
2 | | lsatcmp.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) |
3 | | lveclmod 20143 |
. . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) |
5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
6 | | eqid 2737 |
. . . . 5
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
7 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑊) = (0g‘𝑊) |
8 | | lsatcmp.a |
. . . . 5
⊢ 𝐴 = (LSAtoms‘𝑊) |
9 | 5, 6, 7, 8 | islsat 36742 |
. . . 4
⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}))) |
10 | 4, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}))) |
11 | 1, 10 | mpbid 235 |
. 2
⊢ (𝜑 → ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣})) |
12 | | eldifsn 4700 |
. . . . 5
⊢ (𝑣 ∈ ((Base‘𝑊) ∖
{(0g‘𝑊)})
↔ (𝑣 ∈
(Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) |
13 | | lsatcmp.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
14 | 7, 8, 4, 13 | lsatn0 36750 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≠ {(0g‘𝑊)}) |
15 | 14 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 ≠ {(0g‘𝑊)}) |
16 | 2 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑊 ∈ LVec) |
17 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
18 | 17, 8, 4, 13 | lsatlssel 36748 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑊)) |
19 | 18 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 ∈ (LSubSp‘𝑊)) |
20 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑣 ∈ (Base‘𝑊)) |
21 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) |
22 | 5, 7, 17, 6 | lspsnat 20182 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑇 ∈ (LSubSp‘𝑊) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (𝑇 = ((LSpan‘𝑊)‘{𝑣}) ∨ 𝑇 = {(0g‘𝑊)})) |
23 | 16, 19, 20, 21, 22 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (𝑇 = ((LSpan‘𝑊)‘{𝑣}) ∨ 𝑇 = {(0g‘𝑊)})) |
24 | 23 | ord 864 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (¬ 𝑇 = ((LSpan‘𝑊)‘{𝑣}) → 𝑇 = {(0g‘𝑊)})) |
25 | 24 | necon1ad 2957 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (𝑇 ≠ {(0g‘𝑊)} → 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
26 | 15, 25 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 = ((LSpan‘𝑊)‘{𝑣})) |
27 | 26 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) → 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
28 | | eqimss 3957 |
. . . . . . 7
⊢ (𝑇 = ((LSpan‘𝑊)‘{𝑣}) → 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) |
29 | 27, 28 | impbid1 228 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
30 | 29 | ex 416 |
. . . . 5
⊢ (𝜑 → ((𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊)) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
31 | 12, 30 | syl5bi 245 |
. . . 4
⊢ (𝜑 → (𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
32 | | sseq2 3927 |
. . . . . 6
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}))) |
33 | | eqeq2 2749 |
. . . . . 6
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 = 𝑈 ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
34 | 32, 33 | bibi12d 349 |
. . . . 5
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → ((𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈) ↔ (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
35 | 34 | biimprcd 253 |
. . . 4
⊢ ((𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})) → (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))) |
36 | 31, 35 | syl6 35 |
. . 3
⊢ (𝜑 → (𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) → (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)))) |
37 | 36 | rexlimdv 3202 |
. 2
⊢ (𝜑 → (∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))) |
38 | 11, 37 | mpd 15 |
1
⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) |