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