Metamath Proof Explorer

Theorem lcvp

Description: Covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 10-Jan-2015)

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

    Proof

    Step Hyp Ref Expression
    1 lcvp.s 
     |-  S = ( LSubSp ` W )
    2 lcvp.p 
     |-  .(+) = ( LSSum ` W )
    3 lcvp.o 
     |-  .0. = ( 0g ` W )
    4 lcvp.a 
     |-  A = ( LSAtoms ` W )
    5 lcvp.c 
     |-  C = (
      6 lcvp.w 
       |-  ( ph -> W e. LVec )
      7 lcvp.u 
       |-  ( ph -> U e. S )
      8 lcvp.q 
       |-  ( ph -> Q e. A )
      9 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      10 6 9 syl 
       |-  ( ph -> W e. LMod )
      11 1 4 10 8 lsatlssel 
       |-  ( ph -> Q e. S )
      12 1 lssincl 
       |-  ( ( W e. LMod /\ U e. S /\ Q e. S ) -> ( U i^i Q ) e. S )
      13 10 7 11 12 syl3anc 
       |-  ( ph -> ( U i^i Q ) e. S )
      14 3 1 4 5 6 13 8 lsatcveq0 
       |-  ( ph -> ( ( U i^i Q ) C Q <-> ( U i^i Q ) = { .0. } ) )
      15 1 2 5 10 7 11 lcvexch 
       |-  ( ph -> ( ( U i^i Q ) C Q <-> U C ( U .(+) Q ) ) )
      16 14 15 bitr3d 
       |-  ( ph -> ( ( U i^i Q ) = { .0. } <-> U C ( U .(+) Q ) ) )