Metamath Proof Explorer

Theorem lsatcv0eq

Description: If the sum of two atoms cover the zero subspace, they are equal. ( atcv0eq analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsatcv0eq.o 
|- .0. = ( 0g ` W )
lsatcv0eq.p 
|- .(+) = ( LSSum ` W )
lsatcv0eq.a 
|- A = ( LSAtoms ` W )
lsatcv0eq.c 
|- C = (
    lsatcv0eq.w 
    |- ( ph -> W e. LVec )
    lsatcv0eq.q 
    |- ( ph -> Q e. A )
    lsatcv0eq.r 
    |- ( ph -> R e. A )
    Assertion lsatcv0eq 
    |- ( ph -> ( { .0. } C ( Q .(+) R ) <-> Q = R ) )

    Proof

    Step Hyp Ref Expression
    1 lsatcv0eq.o 
     |-  .0. = ( 0g ` W )
    2 lsatcv0eq.p 
     |-  .(+) = ( LSSum ` W )
    3 lsatcv0eq.a 
     |-  A = ( LSAtoms ` W )
    4 lsatcv0eq.c 
     |-  C = (
      5 lsatcv0eq.w 
       |-  ( ph -> W e. LVec )
      6 lsatcv0eq.q 
       |-  ( ph -> Q e. A )
      7 lsatcv0eq.r 
       |-  ( ph -> R e. A )
      8 1 3 5 6 7 lsatnem0 
       |-  ( ph -> ( Q =/= R <-> ( Q i^i R ) = { .0. } ) )
      9 eqid 
       |-  ( LSubSp ` W ) = ( LSubSp ` W )
      10 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      11 5 10 syl 
       |-  ( ph -> W e. LMod )
      12 9 3 11 6 lsatlssel 
       |-  ( ph -> Q e. ( LSubSp ` W ) )
      13 9 2 1 3 4 5 12 7 lcvp 
       |-  ( ph -> ( ( Q i^i R ) = { .0. } <-> Q C ( Q .(+) R ) ) )
      14 1 3 4 5 6 lsatcv0 
       |-  ( ph -> { .0. } C Q )
      15 14 biantrurd 
       |-  ( ph -> ( Q C ( Q .(+) R ) <-> ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) )
      16 8 13 15 3bitrd 
       |-  ( ph -> ( Q =/= R <-> ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) )
      17 5 adantr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> W e. LVec )
      18 1 9 lsssn0 
       |-  ( W e. LMod -> { .0. } e. ( LSubSp ` W ) )
      19 11 18 syl 
       |-  ( ph -> { .0. } e. ( LSubSp ` W ) )
      20 19 adantr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> { .0. } e. ( LSubSp ` W ) )
      21 12 adantr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> Q e. ( LSubSp ` W ) )
      22 9 3 11 7 lsatlssel 
       |-  ( ph -> R e. ( LSubSp ` W ) )
      23 9 2 lsmcl 
       |-  ( ( W e. LMod /\ Q e. ( LSubSp ` W ) /\ R e. ( LSubSp ` W ) ) -> ( Q .(+) R ) e. ( LSubSp ` W ) )
      24 11 12 22 23 syl3anc 
       |-  ( ph -> ( Q .(+) R ) e. ( LSubSp ` W ) )
      25 24 adantr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> ( Q .(+) R ) e. ( LSubSp ` W ) )
      26 simprl 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> { .0. } C Q )
      27 simprr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> Q C ( Q .(+) R ) )
      28 9 4 17 20 21 25 26 27 lcvntr 
       |-  ( ( ph /\ ( { .0. } C Q /\ Q C ( Q .(+) R ) ) ) -> -. { .0. } C ( Q .(+) R ) )
      29 28 ex 
       |-  ( ph -> ( ( { .0. } C Q /\ Q C ( Q .(+) R ) ) -> -. { .0. } C ( Q .(+) R ) ) )
      30 16 29 sylbid 
       |-  ( ph -> ( Q =/= R -> -. { .0. } C ( Q .(+) R ) ) )
      31 30 necon4ad 
       |-  ( ph -> ( { .0. } C ( Q .(+) R ) -> Q = R ) )
      32 9 lsssssubg 
       |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
      33 11 32 syl 
       |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
      34 33 12 sseldd 
       |-  ( ph -> Q e. ( SubGrp ` W ) )
      35 2 lsmidm 
       |-  ( Q e. ( SubGrp ` W ) -> ( Q .(+) Q ) = Q )
      36 34 35 syl 
       |-  ( ph -> ( Q .(+) Q ) = Q )
      37 14 36 breqtrrd 
       |-  ( ph -> { .0. } C ( Q .(+) Q ) )
      38 oveq2 
       |-  ( Q = R -> ( Q .(+) Q ) = ( Q .(+) R ) )
      39 38 breq2d 
       |-  ( Q = R -> ( { .0. } C ( Q .(+) Q ) <-> { .0. } C ( Q .(+) R ) ) )
      40 37 39 syl5ibcom 
       |-  ( ph -> ( Q = R -> { .0. } C ( Q .(+) R ) ) )
      41 31 40 impbid 
       |-  ( ph -> ( { .0. } C ( Q .(+) R ) <-> Q = R ) )