Metamath Proof Explorer


Theorem lsmcv2

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. ( spansncv2 analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsmcv2.v
|- V = ( Base ` W )
lsmcv2.s
|- S = ( LSubSp ` W )
lsmcv2.n
|- N = ( LSpan ` W )
lsmcv2.p
|- .(+) = ( LSSum ` W )
lsmcv2.c
|- C = ( 
    lsmcv2.w
    |- ( ph -> W e. LVec )
    lsmcv2.u
    |- ( ph -> U e. S )
    lsmcv2.x
    |- ( ph -> X e. V )
    lsmcv2.l
    |- ( ph -> -. ( N ` { X } ) C_ U )
    Assertion lsmcv2
    |- ( ph -> U C ( U .(+) ( N ` { X } ) ) )

    Proof

    Step Hyp Ref Expression
    1 lsmcv2.v
     |-  V = ( Base ` W )
    2 lsmcv2.s
     |-  S = ( LSubSp ` W )
    3 lsmcv2.n
     |-  N = ( LSpan ` W )
    4 lsmcv2.p
     |-  .(+) = ( LSSum ` W )
    5 lsmcv2.c
     |-  C = ( 
      6 lsmcv2.w
       |-  ( ph -> W e. LVec )
      7 lsmcv2.u
       |-  ( ph -> U e. S )
      8 lsmcv2.x
       |-  ( ph -> X e. V )
      9 lsmcv2.l
       |-  ( ph -> -. ( N ` { X } ) C_ U )
      10 lveclmod
       |-  ( W e. LVec -> W e. LMod )
      11 6 10 syl
       |-  ( ph -> W e. LMod )
      12 2 lsssssubg
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      13 11 12 syl
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      14 13 7 sseldd
       |-  ( ph -> U e. ( SubGrp ` W ) )
      15 1 2 3 lspsncl
       |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S )
      16 11 8 15 syl2anc
       |-  ( ph -> ( N ` { X } ) e. S )
      17 13 16 sseldd
       |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
      18 4 14 17 lssnle
       |-  ( ph -> ( -. ( N ` { X } ) C_ U <-> U C. ( U .(+) ( N ` { X } ) ) ) )
      19 9 18 mpbid
       |-  ( ph -> U C. ( U .(+) ( N ` { X } ) ) )
      20 3simpa
       |-  ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> ( ph /\ x e. S ) )
      21 simp3l
       |-  ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> U C. x )
      22 simp3r
       |-  ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> x C_ ( U .(+) ( N ` { X } ) ) )
      23 6 adantr
       |-  ( ( ph /\ x e. S ) -> W e. LVec )
      24 7 adantr
       |-  ( ( ph /\ x e. S ) -> U e. S )
      25 simpr
       |-  ( ( ph /\ x e. S ) -> x e. S )
      26 8 adantr
       |-  ( ( ph /\ x e. S ) -> X e. V )
      27 1 2 3 4 23 24 25 26 lsmcv
       |-  ( ( ( ph /\ x e. S ) /\ U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) )
      28 20 21 22 27 syl3anc
       |-  ( ( ph /\ x e. S /\ ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) ) -> x = ( U .(+) ( N ` { X } ) ) )
      29 28 3exp
       |-  ( ph -> ( x e. S -> ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) ) )
      30 29 ralrimiv
       |-  ( ph -> A. x e. S ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) )
      31 2 4 lsmcl
       |-  ( ( W e. LMod /\ U e. S /\ ( N ` { X } ) e. S ) -> ( U .(+) ( N ` { X } ) ) e. S )
      32 11 7 16 31 syl3anc
       |-  ( ph -> ( U .(+) ( N ` { X } ) ) e. S )
      33 2 5 6 7 32 lcvbr2
       |-  ( ph -> ( U C ( U .(+) ( N ` { X } ) ) <-> ( U C. ( U .(+) ( N ` { X } ) ) /\ A. x e. S ( ( U C. x /\ x C_ ( U .(+) ( N ` { X } ) ) ) -> x = ( U .(+) ( N ` { X } ) ) ) ) ) )
      34 19 30 33 mpbir2and
       |-  ( ph -> U C ( U .(+) ( N ` { X } ) ) )