# Metamath Proof Explorer

## Theorem lsat0cv

Description: A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses lsat0cv.o
lsat0cv.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lsat0cv.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
lsat0cv.c ${⊢}{C}={⋖}_{L}\left({W}\right)$
lsat0cv.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lsat0cv.u ${⊢}{\phi }\to {U}\in {S}$
Assertion lsat0cv

### Proof

Step Hyp Ref Expression
1 lsat0cv.o
2 lsat0cv.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 lsat0cv.a ${⊢}{A}=\mathrm{LSAtoms}\left({W}\right)$
4 lsat0cv.c ${⊢}{C}={⋖}_{L}\left({W}\right)$
5 lsat0cv.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
6 lsat0cv.u ${⊢}{\phi }\to {U}\in {S}$
7 5 adantr ${⊢}\left({\phi }\wedge {U}\in {A}\right)\to {W}\in \mathrm{LVec}$
8 simpr ${⊢}\left({\phi }\wedge {U}\in {A}\right)\to {U}\in {A}$
9 1 3 4 7 8 lsatcv0
10 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
11 5 10 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
13 1 2 lsssn0
14 11 13 syl
17 simpr
18 2 4 12 15 16 17 lcvpss
19 pssnel
20 18 19 syl
22 simprl
23 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
24 23 2 lssel ${⊢}\left({U}\in {S}\wedge {x}\in {U}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
25 21 22 24 syl2anc
26 velsn
27 26 biimpri
28 27 necon3bi
31 eldifsn
32 25 30 31 sylanbrc
33 32 22 jca
34 33 ex
35 34 eximdv
36 df-rex
37 35 36 syl6ibr
38 20 37 mpd
39 simpllr
40 2 4 5 14 6 lcvbr2
45 eldifi
48 eqid ${⊢}\mathrm{LSpan}\left({W}\right)=\mathrm{LSpan}\left({W}\right)$
49 23 2 48 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to \mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\in {S}$
50 44 47 49 syl2anc
51 1 2 lss0ss
52 44 50 51 syl2anc
53 eldifsni
56 23 1 48 lspsneq0
57 44 47 56 syl2anc
58 57 necon3bid
59 55 58 mpbird
60 59 necomd
61 df-pss
62 52 60 61 sylanbrc
65 simplr
66 2 48 44 64 65 lspsnel5a
67 62 66 jca
68 psseq2
69 sseq1 ${⊢}{s}=\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\to \left({s}\subseteq {U}↔\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\subseteq {U}\right)$
70 68 69 anbi12d
71 eqeq1 ${⊢}{s}=\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)\to \left({s}={U}↔\mathrm{LSpan}\left({W}\right)\left(\left\{{x}\right\}\right)={U}\right)$
72 70 71 imbi12d
73 72 rspcv
74 50 73 syl
75 67 74 mpid
76 75 expimpd
77 42 76 sylbid
78 39 77 mpd
79 78 eqcomd
80 79 ex
81 80 reximdva
82 38 81 mpd