Metamath Proof Explorer

Theorem lsatcv0

Description: An atom covers the zero subspace. ( atcv0 analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lsatcv0.o 
|- .0. = ( 0g ` W )
lsatcv0.a 
|- A = ( LSAtoms ` W )
lsatcv0.c 
|- C = (
    lsatcv0.w 
    |- ( ph -> W e. LVec )
    lsatcv0.q 
    |- ( ph -> Q e. A )
    Assertion lsatcv0 
    |- ( ph -> { .0. } C Q )

    Proof

    Step Hyp Ref Expression
    1 lsatcv0.o 
     |-  .0. = ( 0g ` W )
    2 lsatcv0.a 
     |-  A = ( LSAtoms ` W )
    3 lsatcv0.c 
     |-  C = (
      4 lsatcv0.w 
       |-  ( ph -> W e. LVec )
      5 lsatcv0.q 
       |-  ( ph -> Q e. A )
      6 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      7 4 6 syl 
       |-  ( ph -> W e. LMod )
      8 eqid 
       |-  ( LSubSp ` W ) = ( LSubSp ` W )
      9 8 2 7 5 lsatlssel 
       |-  ( ph -> Q e. ( LSubSp ` W ) )
      10 1 8 lss0ss 
       |-  ( ( W e. LMod /\ Q e. ( LSubSp ` W ) ) -> { .0. } C_ Q )
      11 7 9 10 syl2anc 
       |-  ( ph -> { .0. } C_ Q )
      12 1 2 7 5 lsatn0 
       |-  ( ph -> Q =/= { .0. } )
      13 12 necomd 
       |-  ( ph -> { .0. } =/= Q )
      14 df-pss 
       |-  ( { .0. } C. Q <-> ( { .0. } C_ Q /\ { .0. } =/= Q ) )
      15 11 13 14 sylanbrc 
       |-  ( ph -> { .0. } C. Q )
      16 eqid 
       |-  ( Base ` W ) = ( Base ` W )
      17 eqid 
       |-  ( LSpan ` W ) = ( LSpan ` W )
      18 16 17 1 2 islsat 
       |-  ( W e. LMod -> ( Q e. A <-> E. x e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { x } ) ) )
      19 7 18 syl 
       |-  ( ph -> ( Q e. A <-> E. x e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { x } ) ) )
      20 5 19 mpbid 
       |-  ( ph -> E. x e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { x } ) )
      21 4 adantr 
       |-  ( ( ph /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> W e. LVec )
      22 eldifi 
       |-  ( x e. ( ( Base ` W ) \ { .0. } ) -> x e. ( Base ` W ) )
      23 22 adantl 
       |-  ( ( ph /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> x e. ( Base ` W ) )
      24 16 1 8 17 21 23 lspsncv0 
       |-  ( ( ph /\ x e. ( ( Base ` W ) \ { .0. } ) ) -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) )
      25 24 ex 
       |-  ( ph -> ( x e. ( ( Base ` W ) \ { .0. } ) -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) ) )
      26 psseq2 
       |-  ( Q = ( ( LSpan ` W ) ` { x } ) -> ( s C. Q <-> s C. ( ( LSpan ` W ) ` { x } ) ) )
      27 26 anbi2d 
       |-  ( Q = ( ( LSpan ` W ) ` { x } ) -> ( ( { .0. } C. s /\ s C. Q ) <-> ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) ) )
      28 27 rexbidv 
       |-  ( Q = ( ( LSpan ` W ) ` { x } ) -> ( E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) <-> E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) ) )
      29 28 notbid 
       |-  ( Q = ( ( LSpan ` W ) ` { x } ) -> ( -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) <-> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) ) )
      30 29 biimprcd 
       |-  ( -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. ( ( LSpan ` W ) ` { x } ) ) -> ( Q = ( ( LSpan ` W ) ` { x } ) -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) ) )
      31 25 30 syl6 
       |-  ( ph -> ( x e. ( ( Base ` W ) \ { .0. } ) -> ( Q = ( ( LSpan ` W ) ` { x } ) -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) ) ) )
      32 31 rexlimdv 
       |-  ( ph -> ( E. x e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { x } ) -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) ) )
      33 20 32 mpd 
       |-  ( ph -> -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) )
      34 1 8 lsssn0 
       |-  ( W e. LMod -> { .0. } e. ( LSubSp ` W ) )
      35 7 34 syl 
       |-  ( ph -> { .0. } e. ( LSubSp ` W ) )
      36 8 3 4 35 9 lcvbr 
       |-  ( ph -> ( { .0. } C Q <-> ( { .0. } C. Q /\ -. E. s e. ( LSubSp ` W ) ( { .0. } C. s /\ s C. Q ) ) ) )
      37 15 33 36 mpbir2and 
       |-  ( ph -> { .0. } C Q )