Metamath Proof Explorer

Theorem lcv1

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

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

    Proof

    Step Hyp Ref Expression
    1 lcv1.s 
     |-  S = ( LSubSp ` W )
    2 lcv1.p 
     |-  .(+) = ( LSSum ` W )
    3 lcv1.a 
     |-  A = ( LSAtoms ` W )
    4 lcv1.c 
     |-  C = (
      5 lcv1.w 
       |-  ( ph -> W e. LVec )
      6 lcv1.u 
       |-  ( ph -> U e. S )
      7 lcv1.q 
       |-  ( ph -> Q e. A )
      8 eqid 
       |-  ( Base ` W ) = ( Base ` W )
      9 eqid 
       |-  ( LSpan ` W ) = ( LSpan ` W )
      10 eqid 
       |-  ( 0g ` W ) = ( 0g ` W )
      11 8 9 10 3 islsat 
       |-  ( W e. LVec -> ( Q e. A <-> E. x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { x } ) ) )
      12 5 11 syl 
       |-  ( ph -> ( Q e. A <-> E. x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { x } ) ) )
      13 7 12 mpbid 
       |-  ( ph -> E. x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { x } ) )
      14 13 adantr 
       |-  ( ( ph /\ -. Q C_ U ) -> E. x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { x } ) )
      15 5 adantr 
       |-  ( ( ph /\ -. Q C_ U ) -> W e. LVec )
      16 15 3ad2ant1 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> W e. LVec )
      17 6 adantr 
       |-  ( ( ph /\ -. Q C_ U ) -> U e. S )
      18 17 3ad2ant1 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> U e. S )
      19 eldifi 
       |-  ( x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) -> x e. ( Base ` W ) )
      20 19 3ad2ant2 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> x e. ( Base ` W ) )
      21 simp1r 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> -. Q C_ U )
      22 simp3 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> Q = ( ( LSpan ` W ) ` { x } ) )
      23 22 sseq1d 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> ( Q C_ U <-> ( ( LSpan ` W ) ` { x } ) C_ U ) )
      24 21 23 mtbid 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> -. ( ( LSpan ` W ) ` { x } ) C_ U )
      25 8 1 9 2 4 16 18 20 24 lsmcv2 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> U C ( U .(+) ( ( LSpan ` W ) ` { x } ) ) )
      26 22 oveq2d 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> ( U .(+) Q ) = ( U .(+) ( ( LSpan ` W ) ` { x } ) ) )
      27 25 26 breqtrrd 
       |-  ( ( ( ph /\ -. Q C_ U ) /\ x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) /\ Q = ( ( LSpan ` W ) ` { x } ) ) -> U C ( U .(+) Q ) )
      28 27 rexlimdv3a 
       |-  ( ( ph /\ -. Q C_ U ) -> ( E. x e. ( ( Base ` W ) \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { x } ) -> U C ( U .(+) Q ) ) )
      29 14 28 mpd 
       |-  ( ( ph /\ -. Q C_ U ) -> U C ( U .(+) Q ) )
      30 5 adantr 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> W e. LVec )
      31 6 adantr 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> U e. S )
      32 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      33 5 32 syl 
       |-  ( ph -> W e. LMod )
      34 1 3 33 7 lsatlssel 
       |-  ( ph -> Q e. S )
      35 1 2 lsmcl 
       |-  ( ( W e. LMod /\ U e. S /\ Q e. S ) -> ( U .(+) Q ) e. S )
      36 33 6 34 35 syl3anc 
       |-  ( ph -> ( U .(+) Q ) e. S )
      37 36 adantr 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> ( U .(+) Q ) e. S )
      38 simpr 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> U C ( U .(+) Q ) )
      39 1 4 30 31 37 38 lcvpss 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> U C. ( U .(+) Q ) )
      40 1 lsssssubg 
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      41 33 40 syl 
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      42 41 6 sseldd 
       |-  ( ph -> U e. ( SubGrp ` W ) )
      43 41 34 sseldd 
       |-  ( ph -> Q e. ( SubGrp ` W ) )
      44 2 42 43 lssnle 
       |-  ( ph -> ( -. Q C_ U <-> U C. ( U .(+) Q ) ) )
      45 44 adantr 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> ( -. Q C_ U <-> U C. ( U .(+) Q ) ) )
      46 39 45 mpbird 
       |-  ( ( ph /\ U C ( U .(+) Q ) ) -> -. Q C_ U )
      47 29 46 impbida 
       |-  ( ph -> ( -. Q C_ U <-> U C ( U .(+) Q ) ) )