| Step | Hyp | Ref
| Expression |
| 1 | | elfvex 6944 |
. . 3
⊢ (𝑈 ∈ (LSubSp‘𝑊) → 𝑊 ∈ V) |
| 2 | | lssset.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
| 3 | 1, 2 | eleq2s 2859 |
. 2
⊢ (𝑈 ∈ 𝑆 → 𝑊 ∈ V) |
| 4 | | lssset.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
| 5 | | fvprc 6898 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
| 6 | 4, 5 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝑉 = ∅) |
| 7 | 6 | sseq2d 4016 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → (𝑈 ⊆ 𝑉 ↔ 𝑈 ⊆ ∅)) |
| 8 | 7 | biimpcd 249 |
. . . . . 6
⊢ (𝑈 ⊆ 𝑉 → (¬ 𝑊 ∈ V → 𝑈 ⊆ ∅)) |
| 9 | | ss0 4402 |
. . . . . 6
⊢ (𝑈 ⊆ ∅ → 𝑈 = ∅) |
| 10 | 8, 9 | syl6 35 |
. . . . 5
⊢ (𝑈 ⊆ 𝑉 → (¬ 𝑊 ∈ V → 𝑈 = ∅)) |
| 11 | 10 | necon1ad 2957 |
. . . 4
⊢ (𝑈 ⊆ 𝑉 → (𝑈 ≠ ∅ → 𝑊 ∈ V)) |
| 12 | 11 | imp 406 |
. . 3
⊢ ((𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅) → 𝑊 ∈ V) |
| 13 | 12 | 3adant3 1133 |
. 2
⊢ ((𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈) → 𝑊 ∈ V) |
| 14 | | lssset.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
| 15 | | lssset.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐹) |
| 16 | | lssset.p |
. . . . 5
⊢ + =
(+g‘𝑊) |
| 17 | | lssset.t |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
| 18 | 14, 15, 4, 16, 17, 2 | lssset 20931 |
. . . 4
⊢ (𝑊 ∈ V → 𝑆 = {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠}) |
| 19 | 18 | eleq2d 2827 |
. . 3
⊢ (𝑊 ∈ V → (𝑈 ∈ 𝑆 ↔ 𝑈 ∈ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠})) |
| 20 | | eldifsn 4786 |
. . . . . 6
⊢ (𝑈 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅)) |
| 21 | 4 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
| 22 | 21 | elpw2 5334 |
. . . . . . 7
⊢ (𝑈 ∈ 𝒫 𝑉 ↔ 𝑈 ⊆ 𝑉) |
| 23 | 22 | anbi1i 624 |
. . . . . 6
⊢ ((𝑈 ∈ 𝒫 𝑉 ∧ 𝑈 ≠ ∅) ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅)) |
| 24 | 20, 23 | bitri 275 |
. . . . 5
⊢ (𝑈 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅)) |
| 25 | 24 | anbi1i 624 |
. . . 4
⊢ ((𝑈 ∈ (𝒫 𝑉 ∖ {∅}) ∧
∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈) ↔ ((𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 26 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑠 = 𝑈 → (((𝑥 · 𝑎) + 𝑏) ∈ 𝑠 ↔ ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 27 | 26 | raleqbi1dv 3338 |
. . . . . . 7
⊢ (𝑠 = 𝑈 → (∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠 ↔ ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 28 | 27 | raleqbi1dv 3338 |
. . . . . 6
⊢ (𝑠 = 𝑈 → (∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠 ↔ ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 29 | 28 | ralbidv 3178 |
. . . . 5
⊢ (𝑠 = 𝑈 → (∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 30 | 29 | elrab 3692 |
. . . 4
⊢ (𝑈 ∈ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠} ↔ (𝑈 ∈ (𝒫 𝑉 ∖ {∅}) ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 31 | | df-3an 1089 |
. . . 4
⊢ ((𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈) ↔ ((𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅) ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 32 | 25, 30, 31 | 3bitr4i 303 |
. . 3
⊢ (𝑈 ∈ {𝑠 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑠} ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |
| 33 | 19, 32 | bitrdi 287 |
. 2
⊢ (𝑊 ∈ V → (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈))) |
| 34 | 3, 13, 33 | pm5.21nii 378 |
1
⊢ (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ 𝑈 ∀𝑏 ∈ 𝑈 ((𝑥 · 𝑎) + 𝑏) ∈ 𝑈)) |