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 ) ) )