Metamath Proof Explorer

Theorem l1cvpat

Description: A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. ( 1cvrjat analog.) (Contributed by NM, 11-Jan-2015)

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

    Proof

    Step Hyp Ref Expression
    1 l1cvpat.v 
     |-  V = ( Base ` W )
    2 l1cvpat.s 
     |-  S = ( LSubSp ` W )
    3 l1cvpat.p 
     |-  .(+) = ( LSSum ` W )
    4 l1cvpat.a 
     |-  A = ( LSAtoms ` W )
    5 l1cvpat.c 
     |-  C = (
      6 l1cvpat.w 
       |-  ( ph -> W e. LVec )
      7 l1cvpat.u 
       |-  ( ph -> U e. S )
      8 l1cvpat.q 
       |-  ( ph -> Q e. A )
      9 l1cvpat.l 
       |-  ( ph -> U C V )
      10 l1cvpat.m 
       |-  ( ph -> -. Q C_ U )
      11 eqid 
       |-  ( LSpan ` W ) = ( LSpan ` W )
      12 eqid 
       |-  ( 0g ` W ) = ( 0g ` W )
      13 1 11 12 4 islsat 
       |-  ( W e. LVec -> ( Q e. A <-> E. v e. ( V \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { v } ) ) )
      14 6 13 syl 
       |-  ( ph -> ( Q e. A <-> E. v e. ( V \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { v } ) ) )
      15 8 14 mpbid 
       |-  ( ph -> E. v e. ( V \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { v } ) )
      16 eldifi 
       |-  ( v e. ( V \ { ( 0g ` W ) } ) -> v e. V )
      17 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      18 6 17 syl 
       |-  ( ph -> W e. LMod )
      19 18 3ad2ant1 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> W e. LMod )
      20 7 3ad2ant1 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> U e. S )
      21 simp2 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> v e. V )
      22 1 2 11 19 20 21 ellspsn5b 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( v e. U <-> ( ( LSpan ` W ) ` { v } ) C_ U ) )
      23 22 notbid 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( -. v e. U <-> -. ( ( LSpan ` W ) ` { v } ) C_ U ) )
      24 eqid 
       |-  ( LSHyp ` W ) = ( LSHyp ` W )
      25 6 3ad2ant1 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> W e. LVec )
      26 1 2 24 5 6 islshpcv 
       |-  ( ph -> ( U e. ( LSHyp ` W ) <-> ( U e. S /\ U C V ) ) )
      27 7 9 26 mpbir2and 
       |-  ( ph -> U e. ( LSHyp ` W ) )
      28 27 3ad2ant1 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> U e. ( LSHyp ` W ) )
      29 1 11 3 24 25 28 21 lshpnelb 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( -. v e. U <-> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
      30 29 biimpd 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( -. v e. U -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
      31 23 30 sylbird 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( -. ( ( LSpan ` W ) ` { v } ) C_ U -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
      32 sseq1 
       |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( Q C_ U <-> ( ( LSpan ` W ) ` { v } ) C_ U ) )
      33 32 notbid 
       |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( -. Q C_ U <-> -. ( ( LSpan ` W ) ` { v } ) C_ U ) )
      34 oveq2 
       |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( U .(+) Q ) = ( U .(+) ( ( LSpan ` W ) ` { v } ) ) )
      35 34 eqeq1d 
       |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( ( U .(+) Q ) = V <-> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) )
      36 33 35 imbi12d 
       |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( ( -. Q C_ U -> ( U .(+) Q ) = V ) <-> ( -. ( ( LSpan ` W ) ` { v } ) C_ U -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
      37 36 3ad2ant3 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( ( -. Q C_ U -> ( U .(+) Q ) = V ) <-> ( -. ( ( LSpan ` W ) ` { v } ) C_ U -> ( U .(+) ( ( LSpan ` W ) ` { v } ) ) = V ) ) )
      38 31 37 mpbird 
       |-  ( ( ph /\ v e. V /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( -. Q C_ U -> ( U .(+) Q ) = V ) )
      39 38 3exp 
       |-  ( ph -> ( v e. V -> ( Q = ( ( LSpan ` W ) ` { v } ) -> ( -. Q C_ U -> ( U .(+) Q ) = V ) ) ) )
      40 16 39 syl5 
       |-  ( ph -> ( v e. ( V \ { ( 0g ` W ) } ) -> ( Q = ( ( LSpan ` W ) ` { v } ) -> ( -. Q C_ U -> ( U .(+) Q ) = V ) ) ) )
      41 40 rexlimdv 
       |-  ( ph -> ( E. v e. ( V \ { ( 0g ` W ) } ) Q = ( ( LSpan ` W ) ` { v } ) -> ( -. Q C_ U -> ( U .(+) Q ) = V ) ) )
      42 15 10 41 mp2d 
       |-  ( ph -> ( U .(+) Q ) = V )