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

Metamath Proof Explorer

Theorem lcv2

Description: Covering property of a subspace plus an atom. ( chcv2 analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcv2.s 
|- S = ( LSubSp ` W )
lcv2.p 
|- .(+) = ( LSSum ` W )
lcv2.a 
|- A = ( LSAtoms ` W )
lcv2.c 
|- C = (
    lcv2.w 
    |- ( ph -> W e. LVec )
    lcv2.u 
    |- ( ph -> U e. S )
    lcv2.q 
    |- ( ph -> Q e. A )
    Assertion lcv2 
    |- ( ph -> ( U C. ( U .(+) Q ) <-> U C ( U .(+) Q ) ) )

    Proof

    Step Hyp Ref Expression
    1 lcv2.s 
     |-  S = ( LSubSp ` W )
    2 lcv2.p 
     |-  .(+) = ( LSSum ` W )
    3 lcv2.a 
     |-  A = ( LSAtoms ` W )
    4 lcv2.c 
     |-  C = (
      5 lcv2.w 
       |-  ( ph -> W e. LVec )
      6 lcv2.u 
       |-  ( ph -> U e. S )
      7 lcv2.q 
       |-  ( ph -> Q e. A )
      8 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      9 5 8 syl 
       |-  ( ph -> W e. LMod )
      10 1 lsssssubg 
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      11 9 10 syl 
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      12 11 6 sseldd 
       |-  ( ph -> U e. ( SubGrp ` W ) )
      13 1 3 9 7 lsatlssel 
       |-  ( ph -> Q e. S )
      14 11 13 sseldd 
       |-  ( ph -> Q e. ( SubGrp ` W ) )
      15 2 12 14 lssnle 
       |-  ( ph -> ( -. Q C_ U <-> U C. ( U .(+) Q ) ) )
      16 1 2 3 4 5 6 7 lcv1 
       |-  ( ph -> ( -. Q C_ U <-> U C ( U .(+) Q ) ) )
      17 15 16 bitr3d 
       |-  ( ph -> ( U C. ( U .(+) Q ) <-> U C ( U .(+) Q ) ) )