Metamath Proof Explorer

Theorem lsatcv1

Description: Two atoms covering the zero subspace are equal. ( atcv1 analog.) (Contributed by NM, 10-Jan-2015)

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

    Proof

    Step Hyp Ref Expression
    1 lsatcv1.o 
     |-  .0. = ( 0g ` W )
    2 lsatcv1.p 
     |-  .(+) = ( LSSum ` W )
    3 lsatcv1.s 
     |-  S = ( LSubSp ` W )
    4 lsatcv1.a 
     |-  A = ( LSAtoms ` W )
    5 lsatcv1.c 
     |-  C = (
      6 lsatcv1.w 
       |-  ( ph -> W e. LVec )
      7 lsatcv1.u 
       |-  ( ph -> U e. S )
      8 lsatcv1.q 
       |-  ( ph -> Q e. A )
      9 lsatcv1.r 
       |-  ( ph -> R e. A )
      10 lsatcv1.l 
       |-  ( ph -> U C ( Q .(+) R ) )
      11 breq1 
       |-  ( U = { .0. } -> ( U C ( Q .(+) R ) <-> { .0. } C ( Q .(+) R ) ) )
      12 10 11 syl5ibcom 
       |-  ( ph -> ( U = { .0. } -> { .0. } C ( Q .(+) R ) ) )
      13 1 2 4 5 6 8 9 lsatcv0eq 
       |-  ( ph -> ( { .0. } C ( Q .(+) R ) <-> Q = R ) )
      14 12 13 sylibd 
       |-  ( ph -> ( U = { .0. } -> Q = R ) )
      15 10 adantr 
       |-  ( ( ph /\ Q = R ) -> U C ( Q .(+) R ) )
      16 6 adantr 
       |-  ( ( ph /\ Q = R ) -> W e. LVec )
      17 7 adantr 
       |-  ( ( ph /\ Q = R ) -> U e. S )
      18 oveq1 
       |-  ( Q = R -> ( Q .(+) R ) = ( R .(+) R ) )
      19 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      20 6 19 syl 
       |-  ( ph -> W e. LMod )
      21 3 4 20 9 lsatlssel 
       |-  ( ph -> R e. S )
      22 3 lsssubg 
       |-  ( ( W e. LMod /\ R e. S ) -> R e. ( SubGrp ` W ) )
      23 20 21 22 syl2anc 
       |-  ( ph -> R e. ( SubGrp ` W ) )
      24 2 lsmidm 
       |-  ( R e. ( SubGrp ` W ) -> ( R .(+) R ) = R )
      25 23 24 syl 
       |-  ( ph -> ( R .(+) R ) = R )
      26 18 25 sylan9eqr 
       |-  ( ( ph /\ Q = R ) -> ( Q .(+) R ) = R )
      27 9 adantr 
       |-  ( ( ph /\ Q = R ) -> R e. A )
      28 26 27 eqeltrd 
       |-  ( ( ph /\ Q = R ) -> ( Q .(+) R ) e. A )
      29 1 3 4 5 16 17 28 lsatcveq0 
       |-  ( ( ph /\ Q = R ) -> ( U C ( Q .(+) R ) <-> U = { .0. } ) )
      30 15 29 mpbid 
       |-  ( ( ph /\ Q = R ) -> U = { .0. } )
      31 30 ex 
       |-  ( ph -> ( Q = R -> U = { .0. } ) )
      32 14 31 impbid 
       |-  ( ph -> ( U = { .0. } <-> Q = R ) )