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 
|- .0. = ( 0g ` W )
lsat0cv.s 
|- S = ( LSubSp ` W )
lsat0cv.a 
|- A = ( LSAtoms ` W )
lsat0cv.c 
|- C = (
    lsat0cv.w 
    |- ( ph -> W e. LVec )
    lsat0cv.u 
    |- ( ph -> U e. S )
    Assertion lsat0cv 
    |- ( ph -> ( U e. A <-> { .0. } C U ) )

    Proof

    Step Hyp Ref Expression
    1 lsat0cv.o 
     |-  .0. = ( 0g ` W )
    2 lsat0cv.s 
     |-  S = ( LSubSp ` W )
    3 lsat0cv.a 
     |-  A = ( LSAtoms ` W )
    4 lsat0cv.c 
     |-  C = (
      5 lsat0cv.w 
       |-  ( ph -> W e. LVec )
      6 lsat0cv.u 
       |-  ( ph -> U e. S )
      7 5 adantr 
       |-  ( ( ph /\ U e. A ) -> W e. LVec )
      8 simpr 
       |-  ( ( ph /\ U e. A ) -> U e. A )
      9 1 3 4 7 8 lsatcv0 
       |-  ( ( ph /\ U e. A ) -> { .0. } C U )
      10 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      11 5 10 syl 
       |-  ( ph -> W e. LMod )
      12 11 adantr 
       |-  ( ( ph /\ { .0. } C U ) -> W e. LMod )
      13 1 2 lsssn0 
       |-  ( W e. LMod -> { .0. } e. S )
      14 11 13 syl 
       |-  ( ph -> { .0. } e. S )
      15 14 adantr 
       |-  ( ( ph /\ { .0. } C U ) -> { .0. } e. S )
      16 6 adantr 
       |-  ( ( ph /\ { .0. } C U ) -> U e. S )
      17 simpr 
       |-  ( ( ph /\ { .0. } C U ) -> { .0. } C U )
      18 2 4 12 15 16 17 lcvpss 
       |-  ( ( ph /\ { .0. } C U ) -> { .0. } C. U )
      19 pssnel 
       |-  ( { .0. } C. U -> E. x ( x e. U /\ -. x e. { .0. } ) )
      20 18 19 syl 
       |-  ( ( ph /\ { .0. } C U ) -> E. x ( x e. U /\ -. x e. { .0. } ) )
      21 6 ad2antrr 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> U e. S )
      22 simprl 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> x e. U )
      23 eqid 
       |-  ( Base ` W ) = ( Base ` W )
      24 23 2 lssel 
       |-  ( ( U e. S /\ x e. U ) -> x e. ( Base ` W ) )
      25 21 22 24 syl2anc 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> x e. ( Base ` W ) )
      26 velsn 
       |-  ( x e. { .0. } <-> x = .0. )
      27 26 biimpri 
       |-  ( x = .0. -> x e. { .0. } )
      28 27 necon3bi 
       |-  ( -. x e. { .0. } -> x =/= .0. )
      29 28 adantl 
       |-  ( ( x e. U /\ -. x e. { .0. } ) -> x =/= .0. )
      30 29 adantl 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> x =/= .0. )
      31 eldifsn 
       |-  ( x e. ( ( Base ` W ) \ { .0. } ) <-> ( x e. ( Base ` W ) /\ x =/= .0. ) )
      32 25 30 31 sylanbrc 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> x e. ( ( Base ` W ) \ { .0. } ) )
      33 32 22 jca 
       |-  ( ( ( ph /\ { .0. } C U ) /\ ( x e. U /\ -. x e. { .0. } ) ) -> ( x e. ( ( Base ` W ) \ { .0. } ) /\ x e. U ) )
      34 33 ex 
       |-  ( ( ph /\ { .0. } C U ) -> ( ( x e. U /\ -. x e. { .0. } ) -> ( x e. ( ( Base ` W ) \ { .0. } ) /\ x e. U ) ) )
      35 34 eximdv 
       |-  ( ( ph /\ { .0. } C U ) -> ( E. x ( x e. U /\ -. x e. { .0. } ) -> E. x ( x e. ( ( Base ` W ) \ { .0. } ) /\ x e. U ) ) )
      36 df-rex 
       |-  ( E. x e. ( ( Base ` W ) \ { .0. } ) x e. U <-> E. x ( x e. ( ( Base ` W ) \ { .0. } ) /\ x e. U ) )
      37 35 36 imbitrrdi 
       |-  ( ( ph /\ { .0. } C U ) -> ( E. x ( x e. U /\ -. x e. { .0. } ) -> E. x e. ( ( Base ` W ) \ { .0. } ) x e. U ) )
      38 20 37 mpd 
       |-  ( ( ph /\ { .0. } C U ) -> E. x e. ( ( Base ` W ) \ { .0. } ) x e. U )
      39 simpllr 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> { .0. } C U )
      40 2 4 5 14 6 lcvbr2 
       |-  ( ph -> ( { .0. } C U <-> ( { .0. } C. U /\ A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) ) ) )
      41 40 adantr 
       |-  ( ( ph /\ { .0. } C U ) -> ( { .0. } C U <-> ( { .0. } C. U /\ A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) ) ) )
      42 41 ad2antrr 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> ( { .0. } C U <-> ( { .0. } C. U /\ A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) ) ) )
      43 11 ad2antrr 
       |-  ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> W e. LMod )
      44 43 ad2antrr 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> W e. LMod )
      45 eldifi 
       |-  ( x e. ( ( Base ` W ) \ { .0. } ) -> x e. ( Base ` W ) )
      46 45 adantl 
       |-  ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> x e. ( Base ` W ) )
      47 46 ad2antrr 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> x e. ( Base ` W ) )
      48 eqid 
       |-  ( LSpan ` W ) = ( LSpan ` W )
      49 23 2 48 lspsncl 
       |-  ( ( W e. LMod /\ x e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { x } ) e. S )
      50 44 47 49 syl2anc 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( ( LSpan ` W ) ` { x } ) e. S )
      51 1 2 lss0ss 
       |-  ( ( W e. LMod /\ ( ( LSpan ` W ) ` { x } ) e. S ) -> { .0. } C_ ( ( LSpan ` W ) ` { x } ) )
      52 44 50 51 syl2anc 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> { .0. } C_ ( ( LSpan ` W ) ` { x } ) )
      53 eldifsni 
       |-  ( x e. ( ( Base ` W ) \ { .0. } ) -> x =/= .0. )
      54 53 adantl 
       |-  ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> x =/= .0. )
      55 54 ad2antrr 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> x =/= .0. )
      56 23 1 48 lspsneq0 
       |-  ( ( W e. LMod /\ x e. ( Base ` W ) ) -> ( ( ( LSpan ` W ) ` { x } ) = { .0. } <-> x = .0. ) )
      57 44 47 56 syl2anc 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( ( ( LSpan ` W ) ` { x } ) = { .0. } <-> x = .0. ) )
      58 57 necon3bid 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( ( ( LSpan ` W ) ` { x } ) =/= { .0. } <-> x =/= .0. ) )
      59 55 58 mpbird 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( ( LSpan ` W ) ` { x } ) =/= { .0. } )
      60 59 necomd 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> { .0. } =/= ( ( LSpan ` W ) ` { x } ) )
      61 df-pss 
       |-  ( { .0. } C. ( ( LSpan ` W ) ` { x } ) <-> ( { .0. } C_ ( ( LSpan ` W ) ` { x } ) /\ { .0. } =/= ( ( LSpan ` W ) ` { x } ) ) )
      62 52 60 61 sylanbrc 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> { .0. } C. ( ( LSpan ` W ) ` { x } ) )
      63 6 ad2antrr 
       |-  ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> U e. S )
      64 63 ad2antrr 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> U e. S )
      65 simplr 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> x e. U )
      66 2 48 44 64 65 ellspsn5 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( ( LSpan ` W ) ` { x } ) C_ U )
      67 62 66 jca 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( { .0. } C. ( ( LSpan ` W ) ` { x } ) /\ ( ( LSpan ` W ) ` { x } ) C_ U ) )
      68 psseq2 
       |-  ( s = ( ( LSpan ` W ) ` { x } ) -> ( { .0. } C. s <-> { .0. } C. ( ( LSpan ` W ) ` { x } ) ) )
      69 sseq1 
       |-  ( s = ( ( LSpan ` W ) ` { x } ) -> ( s C_ U <-> ( ( LSpan ` W ) ` { x } ) C_ U ) )
      70 68 69 anbi12d 
       |-  ( s = ( ( LSpan ` W ) ` { x } ) -> ( ( { .0. } C. s /\ s C_ U ) <-> ( { .0. } C. ( ( LSpan ` W ) ` { x } ) /\ ( ( LSpan ` W ) ` { x } ) C_ U ) ) )
      71 eqeq1 
       |-  ( s = ( ( LSpan ` W ) ` { x } ) -> ( s = U <-> ( ( LSpan ` W ) ` { x } ) = U ) )
      72 70 71 imbi12d 
       |-  ( s = ( ( LSpan ` W ) ` { x } ) -> ( ( ( { .0. } C. s /\ s C_ U ) -> s = U ) <-> ( ( { .0. } C. ( ( LSpan ` W ) ` { x } ) /\ ( ( LSpan ` W ) ` { x } ) C_ U ) -> ( ( LSpan ` W ) ` { x } ) = U ) ) )
      73 72 rspcv 
       |-  ( ( ( LSpan ` W ) ` { x } ) e. S -> ( A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) -> ( ( { .0. } C. ( ( LSpan ` W ) ` { x } ) /\ ( ( LSpan ` W ) ` { x } ) C_ U ) -> ( ( LSpan ` W ) ` { x } ) = U ) ) )
      74 50 73 syl 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) -> ( ( { .0. } C. ( ( LSpan ` W ) ` { x } ) /\ ( ( LSpan ` W ) ` { x } ) C_ U ) -> ( ( LSpan ` W ) ` { x } ) = U ) ) )
      75 67 74 mpid 
       |-  ( ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) /\ { .0. } C. U ) -> ( A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) -> ( ( LSpan ` W ) ` { x } ) = U ) )
      76 75 expimpd 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> ( ( { .0. } C. U /\ A. s e. S ( ( { .0. } C. s /\ s C_ U ) -> s = U ) ) -> ( ( LSpan ` W ) ` { x } ) = U ) )
      77 42 76 sylbid 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> ( { .0. } C U -> ( ( LSpan ` W ) ` { x } ) = U ) )
      78 39 77 mpd 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> ( ( LSpan ` W ) ` { x } ) = U )
      79 78 eqcomd 
       |-  ( ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) /\ x e. U ) -> U = ( ( LSpan ` W ) ` { x } ) )
      80 79 ex 
       |-  ( ( ( ph /\ { .0. } C U ) /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> ( x e. U -> U = ( ( LSpan ` W ) ` { x } ) ) )
      81 80 reximdva 
       |-  ( ( ph /\ { .0. } C U ) -> ( E. x e. ( ( Base ` W ) \ { .0. } ) x e. U -> E. x e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { x } ) ) )
      82 38 81 mpd 
       |-  ( ( ph /\ { .0. } C U ) -> E. x e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { x } ) )
      83 5 adantr 
       |-  ( ( ph /\ { .0. } C U ) -> W e. LVec )
      84 23 48 1 3 islsat 
       |-  ( W e. LVec -> ( U e. A <-> E. x e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { x } ) ) )
      85 83 84 syl 
       |-  ( ( ph /\ { .0. } C U ) -> ( U e. A <-> E. x e. ( ( Base ` W ) \ { .0. } ) U = ( ( LSpan ` W ) ` { x } ) ) )
      86 82 85 mpbird 
       |-  ( ( ph /\ { .0. } C U ) -> U e. A )
      87 9 86 impbida 
       |-  ( ph -> ( U e. A <-> { .0. } C U ) )