This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lssatomic

Description: The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. ( shatomici analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lssatomic.s 
|- S = ( LSubSp ` W )
lssatomic.o 
|- .0. = ( 0g ` W )
lssatomic.a 
|- A = ( LSAtoms ` W )
lssatomic.w 
|- ( ph -> W e. LMod )
lssatomic.u 
|- ( ph -> U e. S )
lssatomic.n 
|- ( ph -> U =/= { .0. } )
Assertion lssatomic 
|- ( ph -> E. q e. A q C_ U )

Proof

Step Hyp Ref Expression
1 lssatomic.s 
 |-  S = ( LSubSp ` W )
2 lssatomic.o 
 |-  .0. = ( 0g ` W )
3 lssatomic.a 
 |-  A = ( LSAtoms ` W )
4 lssatomic.w 
 |-  ( ph -> W e. LMod )
5 lssatomic.u 
 |-  ( ph -> U e. S )
6 lssatomic.n 
 |-  ( ph -> U =/= { .0. } )
7 2 1 lssne0 
 |-  ( U e. S -> ( U =/= { .0. } <-> E. x e. U x =/= .0. ) )
8 5 7 syl 
 |-  ( ph -> ( U =/= { .0. } <-> E. x e. U x =/= .0. ) )
9 6 8 mpbid 
 |-  ( ph -> E. x e. U x =/= .0. )
10 4 3ad2ant1 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> W e. LMod )
11 5 3ad2ant1 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> U e. S )
12 simp2 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> x e. U )
13 eqid 
 |-  ( Base ` W ) = ( Base ` W )
14 13 1 lssel 
 |-  ( ( U e. S /\ x e. U ) -> x e. ( Base ` W ) )
15 11 12 14 syl2anc 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> x e. ( Base ` W ) )
16 simp3 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> x =/= .0. )
17 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
18 13 17 2 3 lsatlspsn2 
 |-  ( ( W e. LMod /\ x e. ( Base ` W ) /\ x =/= .0. ) -> ( ( LSpan ` W ) ` { x } ) e. A )
19 10 15 16 18 syl3anc 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> ( ( LSpan ` W ) ` { x } ) e. A )
20 1 17 10 11 12 ellspsn5 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> ( ( LSpan ` W ) ` { x } ) C_ U )
21 sseq1 
 |-  ( q = ( ( LSpan ` W ) ` { x } ) -> ( q C_ U <-> ( ( LSpan ` W ) ` { x } ) C_ U ) )
22 21 rspcev 
 |-  ( ( ( ( LSpan ` W ) ` { x } ) e. A /\ ( ( LSpan ` W ) ` { x } ) C_ U ) -> E. q e. A q C_ U )
23 19 20 22 syl2anc 
 |-  ( ( ph /\ x e. U /\ x =/= .0. ) -> E. q e. A q C_ U )
24 23 rexlimdv3a 
 |-  ( ph -> ( E. x e. U x =/= .0. -> E. q e. A q C_ U ) )
25 9 24 mpd 
 |-  ( ph -> E. q e. A q C_ U )