Metamath Proof Explorer

Theorem lsatcveq0

Description: A subspace covered by an atom must be the zero subspace. ( atcveq0 analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lsatcveq0.o 
|- .0. = ( 0g ` W )
lsatcveq0.s 
|- S = ( LSubSp ` W )
lsatcveq0.a 
|- A = ( LSAtoms ` W )
lsatcveq0.c 
|- C = (
    lsatcveq0.w 
    |- ( ph -> W e. LVec )
    lsatcveq0.u 
    |- ( ph -> U e. S )
    lsatcveq0.q 
    |- ( ph -> Q e. A )
    Assertion lsatcveq0 
    |- ( ph -> ( U C Q <-> U = { .0. } ) )

    Proof

    Step Hyp Ref Expression
    1 lsatcveq0.o 
     |-  .0. = ( 0g ` W )
    2 lsatcveq0.s 
     |-  S = ( LSubSp ` W )
    3 lsatcveq0.a 
     |-  A = ( LSAtoms ` W )
    4 lsatcveq0.c 
     |-  C = (
      5 lsatcveq0.w 
       |-  ( ph -> W e. LVec )
      6 lsatcveq0.u 
       |-  ( ph -> U e. S )
      7 lsatcveq0.q 
       |-  ( ph -> Q e. A )
      8 5 adantr 
       |-  ( ( ph /\ U C Q ) -> W e. LVec )
      9 6 adantr 
       |-  ( ( ph /\ U C Q ) -> U e. S )
      10 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      11 5 10 syl 
       |-  ( ph -> W e. LMod )
      12 2 3 11 7 lsatlssel 
       |-  ( ph -> Q e. S )
      13 12 adantr 
       |-  ( ( ph /\ U C Q ) -> Q e. S )
      14 simpr 
       |-  ( ( ph /\ U C Q ) -> U C Q )
      15 2 4 8 9 13 14 lcvpss 
       |-  ( ( ph /\ U C Q ) -> U C. Q )
      16 15 ex 
       |-  ( ph -> ( U C Q -> U C. Q ) )
      17 1 3 4 5 7 lsatcv0 
       |-  ( ph -> { .0. } C Q )
      18 5 3ad2ant1 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> W e. LVec )
      19 1 2 lsssn0 
       |-  ( W e. LMod -> { .0. } e. S )
      20 11 19 syl 
       |-  ( ph -> { .0. } e. S )
      21 20 3ad2ant1 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> { .0. } e. S )
      22 12 3ad2ant1 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> Q e. S )
      23 6 3ad2ant1 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> U e. S )
      24 simp2 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> { .0. } C Q )
      25 1 2 lss0ss 
       |-  ( ( W e. LMod /\ U e. S ) -> { .0. } C_ U )
      26 11 6 25 syl2anc 
       |-  ( ph -> { .0. } C_ U )
      27 26 3ad2ant1 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> { .0. } C_ U )
      28 simp3 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> U C. Q )
      29 2 4 18 21 22 23 24 27 28 lcvnbtwn3 
       |-  ( ( ph /\ { .0. } C Q /\ U C. Q ) -> U = { .0. } )
      30 29 3exp 
       |-  ( ph -> ( { .0. } C Q -> ( U C. Q -> U = { .0. } ) ) )
      31 17 30 mpd 
       |-  ( ph -> ( U C. Q -> U = { .0. } ) )
      32 16 31 syld 
       |-  ( ph -> ( U C Q -> U = { .0. } ) )
      33 breq1 
       |-  ( U = { .0. } -> ( U C Q <-> { .0. } C Q ) )
      34 17 33 syl5ibrcom 
       |-  ( ph -> ( U = { .0. } -> U C Q ) )
      35 32 34 impbid 
       |-  ( ph -> ( U C Q <-> U = { .0. } ) )