Step | Hyp | Ref
| Expression |
1 | | lsat0cv.o |
. . 3
⊢ 0 =
(0g‘𝑊) |
2 | | lsat0cv.a |
. . 3
⊢ 𝐴 = (LSAtoms‘𝑊) |
3 | | lsat0cv.c |
. . 3
⊢ 𝐶 = ( ⋖L
‘𝑊) |
4 | | lsat0cv.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LVec) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑈 ∈ 𝐴) → 𝑊 ∈ LVec) |
6 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝑈 ∈ 𝐴) → 𝑈 ∈ 𝐴) |
7 | 1, 2, 3, 5, 6 | lsatcv0 36795 |
. 2
⊢ ((𝜑 ∧ 𝑈 ∈ 𝐴) → { 0 }𝐶𝑈) |
8 | | lsat0cv.s |
. . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑊) |
9 | | lveclmod 20156 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
10 | 4, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → 𝑊 ∈ LMod) |
12 | 1, 8 | lsssn0 19997 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → { 0 } ∈
𝑆) |
13 | 10, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → { 0 } ∈ 𝑆) |
14 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → { 0 } ∈ 𝑆) |
15 | | lsat0cv.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
16 | 15 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → 𝑈 ∈ 𝑆) |
17 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → { 0 }𝐶𝑈) |
18 | 8, 3, 11, 14, 16, 17 | lcvpss 36788 |
. . . . . 6
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → { 0 } ⊊ 𝑈) |
19 | | pssnel 4394 |
. . . . . 6
⊢ ({ 0 } ⊊
𝑈 → ∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → ∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) |
21 | 15 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → 𝑈 ∈ 𝑆) |
22 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → 𝑥 ∈ 𝑈) |
23 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑊) =
(Base‘𝑊) |
24 | 23, 8 | lssel 19987 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑊)) |
25 | 21, 22, 24 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → 𝑥 ∈ (Base‘𝑊)) |
26 | | velsn 4566 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
27 | 26 | biimpri 231 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → 𝑥 ∈ { 0 }) |
28 | 27 | necon3bi 2968 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ∈ { 0 } →
𝑥 ≠ 0 ) |
29 | 28 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 }) → 𝑥 ≠ 0 ) |
30 | 29 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → 𝑥 ≠ 0 ) |
31 | | eldifsn 4709 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) ↔ (𝑥 ∈ (Base‘𝑊) ∧ 𝑥 ≠ 0 )) |
32 | 25, 30, 31 | sylanbrc 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) |
33 | 32, 22 | jca 515 |
. . . . . . . 8
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ (𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 })) → (𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑥 ∈ 𝑈)) |
34 | 33 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → ((𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 }) → (𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑥 ∈ 𝑈))) |
35 | 34 | eximdv 1925 |
. . . . . 6
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → (∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 }) → ∃𝑥(𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑥 ∈ 𝑈))) |
36 | | df-rex 3068 |
. . . . . 6
⊢
(∃𝑥 ∈
((Base‘𝑊) ∖ {
0 })𝑥 ∈ 𝑈 ↔ ∃𝑥(𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑥 ∈ 𝑈)) |
37 | 35, 36 | syl6ibr 255 |
. . . . 5
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → (∃𝑥(𝑥 ∈ 𝑈 ∧ ¬ 𝑥 ∈ { 0 }) → ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑥 ∈ 𝑈)) |
38 | 20, 37 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑥 ∈ 𝑈) |
39 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → { 0 }𝐶𝑈) |
40 | 8, 3, 4, 13, 15 | lcvbr2 36786 |
. . . . . . . . . . 11
⊢ (𝜑 → ({ 0 }𝐶𝑈 ↔ ({ 0 } ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈)))) |
41 | 40 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → ({ 0 }𝐶𝑈 ↔ ({ 0 } ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈)))) |
42 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → ({ 0 }𝐶𝑈 ↔ ({ 0 } ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈)))) |
43 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑊 ∈ LMod) |
44 | 43 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → 𝑊 ∈ LMod) |
45 | | eldifi 4050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) → 𝑥 ∈ (Base‘𝑊)) |
46 | 45 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑥 ∈ (Base‘𝑊)) |
47 | 46 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → 𝑥 ∈ (Base‘𝑊)) |
48 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
49 | 23, 8, 48 | lspsncl 20027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{𝑥}) ∈ 𝑆) |
50 | 44, 47, 49 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) ∈ 𝑆) |
51 | 1, 8 | lss0ss 19998 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧
((LSpan‘𝑊)‘{𝑥}) ∈ 𝑆) → { 0 } ⊆
((LSpan‘𝑊)‘{𝑥})) |
52 | 44, 50, 51 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → { 0 } ⊆
((LSpan‘𝑊)‘{𝑥})) |
53 | | eldifsni 4712 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((Base‘𝑊) ∖ { 0 }) → 𝑥 ≠ 0 ) |
54 | 53 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑥 ≠ 0 ) |
55 | 54 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → 𝑥 ≠ 0 ) |
56 | 23, 1, 48 | lspsneq0 20062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊)) → (((LSpan‘𝑊)‘{𝑥}) = { 0 } ↔ 𝑥 = 0 )) |
57 | 44, 47, 56 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → (((LSpan‘𝑊)‘{𝑥}) = { 0 } ↔ 𝑥 = 0 )) |
58 | 57 | necon3bid 2986 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → (((LSpan‘𝑊)‘{𝑥}) ≠ { 0 } ↔ 𝑥 ≠ 0 )) |
59 | 55, 58 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) ≠ { 0 }) |
60 | 59 | necomd 2997 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → { 0 } ≠ ((LSpan‘𝑊)‘{𝑥})) |
61 | | df-pss 3894 |
. . . . . . . . . . . . 13
⊢ ({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ↔ ({ 0 } ⊆
((LSpan‘𝑊)‘{𝑥}) ∧ { 0 } ≠ ((LSpan‘𝑊)‘{𝑥}))) |
62 | 52, 60, 61 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → { 0 } ⊊
((LSpan‘𝑊)‘{𝑥})) |
63 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑈 ∈ 𝑆) |
64 | 63 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → 𝑈 ∈ 𝑆) |
65 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → 𝑥 ∈ 𝑈) |
66 | 8, 48, 44, 64, 65 | lspsnel5a 20046 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈) |
67 | 62, 66 | jca 515 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → ({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ∧ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈)) |
68 | | psseq2 4012 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = ((LSpan‘𝑊)‘{𝑥}) → ({ 0 } ⊊ 𝑠 ↔ { 0 } ⊊
((LSpan‘𝑊)‘{𝑥}))) |
69 | | sseq1 3935 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = ((LSpan‘𝑊)‘{𝑥}) → (𝑠 ⊆ 𝑈 ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈)) |
70 | 68, 69 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = ((LSpan‘𝑊)‘{𝑥}) → (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) ↔ ({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ∧ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈))) |
71 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = ((LSpan‘𝑊)‘{𝑥}) → (𝑠 = 𝑈 ↔ ((LSpan‘𝑊)‘{𝑥}) = 𝑈)) |
72 | 70, 71 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑠 = ((LSpan‘𝑊)‘{𝑥}) → ((({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈) ↔ (({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ∧ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈))) |
73 | 72 | rspcv 3539 |
. . . . . . . . . . . 12
⊢
(((LSpan‘𝑊)‘{𝑥}) ∈ 𝑆 → (∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈) → (({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ∧ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈))) |
74 | 50, 73 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → (∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈) → (({ 0 } ⊊
((LSpan‘𝑊)‘{𝑥}) ∧ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈))) |
75 | 67, 74 | mpid 44 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) ∧ { 0 } ⊊ 𝑈) → (∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈)) |
76 | 75 | expimpd 457 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → (({ 0 } ⊊ 𝑈 ∧ ∀𝑠 ∈ 𝑆 (({ 0 } ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈) → 𝑠 = 𝑈)) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈)) |
77 | 42, 76 | sylbid 243 |
. . . . . . . 8
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → ({ 0 }𝐶𝑈 → ((LSpan‘𝑊)‘{𝑥}) = 𝑈)) |
78 | 39, 77 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → ((LSpan‘𝑊)‘{𝑥}) = 𝑈) |
79 | 78 | eqcomd 2744 |
. . . . . 6
⊢ ((((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ 𝑥 ∈ 𝑈) → 𝑈 = ((LSpan‘𝑊)‘{𝑥})) |
80 | 79 | ex 416 |
. . . . 5
⊢ (((𝜑 ∧ { 0 }𝐶𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ { 0 })) → (𝑥 ∈ 𝑈 → 𝑈 = ((LSpan‘𝑊)‘{𝑥}))) |
81 | 80 | reximdva 3200 |
. . . 4
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → (∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑥 ∈ 𝑈 → ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑈 = ((LSpan‘𝑊)‘{𝑥}))) |
82 | 38, 81 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑈 = ((LSpan‘𝑊)‘{𝑥})) |
83 | 4 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → 𝑊 ∈ LVec) |
84 | 23, 48, 1, 2 | islsat 36755 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑈 = ((LSpan‘𝑊)‘{𝑥}))) |
85 | 83, 84 | syl 17 |
. . 3
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ { 0 })𝑈 = ((LSpan‘𝑊)‘{𝑥}))) |
86 | 82, 85 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ { 0 }𝐶𝑈) → 𝑈 ∈ 𝐴) |
87 | 7, 86 | impbida 801 |
1
⊢ (𝜑 → (𝑈 ∈ 𝐴 ↔ { 0 }𝐶𝑈)) |