| Step | Hyp | Ref
| Expression |
| 1 | | lsatcmp.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
| 2 | | lsatcmp.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 3 | | lveclmod 21105 |
. . . . 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 38992 |
. . . 4
⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}))) |
| 10 | 4, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}))) |
| 11 | 1, 10 | mpbid 232 |
. 2
⊢ (𝜑 → ∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣})) |
| 12 | | eldifsn 4786 |
. . . . 5
⊢ (𝑣 ∈ ((Base‘𝑊) ∖
{(0g‘𝑊)})
↔ (𝑣 ∈
(Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) |
| 13 | | lsatcmp.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
| 14 | 7, 8, 4, 13 | lsatn0 39000 |
. . . . . . . . . 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 38998 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑊)) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 ∈ (LSubSp‘𝑊)) |
| 20 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑣 ∈ (Base‘𝑊)) |
| 21 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) |
| 22 | 5, 7, 17, 6 | lspsnat 21147 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LVec ∧ 𝑇 ∈ (LSubSp‘𝑊) ∧ 𝑣 ∈ (Base‘𝑊)) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (𝑇 = ((LSpan‘𝑊)‘{𝑣}) ∨ 𝑇 = {(0g‘𝑊)})) |
| 23 | 16, 19, 20, 21, 22 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) ∧ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) → (𝑇 = ((LSpan‘𝑊)‘{𝑣}) ∨ 𝑇 = {(0g‘𝑊)})) |
| 24 | 23 | ord 865 |
. . . . . . . . . 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 412 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) → 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
| 28 | | eqimss 4042 |
. . . . . . 7
⊢ (𝑇 = ((LSpan‘𝑊)‘{𝑣}) → 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣})) |
| 29 | 27, 28 | impbid1 225 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊))) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
| 30 | 29 | ex 412 |
. . . . 5
⊢ (𝜑 → ((𝑣 ∈ (Base‘𝑊) ∧ 𝑣 ≠ (0g‘𝑊)) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
| 31 | 12, 30 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) → (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
| 32 | | sseq2 4010 |
. . . . . 6
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}))) |
| 33 | | eqeq2 2749 |
. . . . . 6
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 = 𝑈 ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣}))) |
| 34 | 32, 33 | bibi12d 345 |
. . . . 5
⊢ (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → ((𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈) ↔ (𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})))) |
| 35 | 34 | biimprcd 250 |
. . . 4
⊢ ((𝑇 ⊆ ((LSpan‘𝑊)‘{𝑣}) ↔ 𝑇 = ((LSpan‘𝑊)‘{𝑣})) → (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))) |
| 36 | 31, 35 | syl6 35 |
. . 3
⊢ (𝜑 → (𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) → (𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)))) |
| 37 | 36 | rexlimdv 3153 |
. 2
⊢ (𝜑 → (∃𝑣 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑈 = ((LSpan‘𝑊)‘{𝑣}) → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈))) |
| 38 | 11, 37 | mpd 15 |
1
⊢ (𝜑 → (𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈)) |