Metamath Proof Explorer


Theorem lsatcvat3

Description: A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lsatcvat3.s
|- S = ( LSubSp ` W )
lsatcvat3.p
|- .(+) = ( LSSum ` W )
lsatcvat3.a
|- A = ( LSAtoms ` W )
lsatcvat3.w
|- ( ph -> W e. LVec )
lsatcvat3.u
|- ( ph -> U e. S )
lsatcvat3.q
|- ( ph -> Q e. A )
lsatcvat3.r
|- ( ph -> R e. A )
lsatcvat3.n
|- ( ph -> Q =/= R )
lsatcvat3.m
|- ( ph -> -. R C_ U )
lsatcvat3.l
|- ( ph -> Q C_ ( U .(+) R ) )
Assertion lsatcvat3
|- ( ph -> ( U i^i ( Q .(+) R ) ) e. A )

Proof

Step Hyp Ref Expression
1 lsatcvat3.s
 |-  S = ( LSubSp ` W )
2 lsatcvat3.p
 |-  .(+) = ( LSSum ` W )
3 lsatcvat3.a
 |-  A = ( LSAtoms ` W )
4 lsatcvat3.w
 |-  ( ph -> W e. LVec )
5 lsatcvat3.u
 |-  ( ph -> U e. S )
6 lsatcvat3.q
 |-  ( ph -> Q e. A )
7 lsatcvat3.r
 |-  ( ph -> R e. A )
8 lsatcvat3.n
 |-  ( ph -> Q =/= R )
9 lsatcvat3.m
 |-  ( ph -> -. R C_ U )
10 lsatcvat3.l
 |-  ( ph -> Q C_ ( U .(+) R ) )
11 eqid
 |-  ( 
    12 lveclmod
     |-  ( W e. LVec -> W e. LMod )
    13 4 12 syl
     |-  ( ph -> W e. LMod )
    14 1 3 13 6 lsatlssel
     |-  ( ph -> Q e. S )
    15 1 3 13 7 lsatlssel
     |-  ( ph -> R e. S )
    16 1 2 lsmcl
     |-  ( ( W e. LMod /\ Q e. S /\ R e. S ) -> ( Q .(+) R ) e. S )
    17 13 14 15 16 syl3anc
     |-  ( ph -> ( Q .(+) R ) e. S )
    18 1 lssincl
     |-  ( ( W e. LMod /\ U e. S /\ ( Q .(+) R ) e. S ) -> ( U i^i ( Q .(+) R ) ) e. S )
    19 13 5 17 18 syl3anc
     |-  ( ph -> ( U i^i ( Q .(+) R ) ) e. S )
    20 1 2 3 11 4 5 7 lcv1
     |-  ( ph -> ( -. R C_ U <-> U ( 
      21 9 20 mpbid
       |-  ( ph -> U ( 
        22 lmodabl
         |-  ( W e. LMod -> W e. Abel )
        23 13 22 syl
         |-  ( ph -> W e. Abel )
        24 1 lsssssubg
         |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
        25 13 24 syl
         |-  ( ph -> S C_ ( SubGrp ` W ) )
        26 25 14 sseldd
         |-  ( ph -> Q e. ( SubGrp ` W ) )
        27 25 15 sseldd
         |-  ( ph -> R e. ( SubGrp ` W ) )
        28 2 lsmcom
         |-  ( ( W e. Abel /\ Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> ( Q .(+) R ) = ( R .(+) Q ) )
        29 23 26 27 28 syl3anc
         |-  ( ph -> ( Q .(+) R ) = ( R .(+) Q ) )
        30 29 oveq2d
         |-  ( ph -> ( U .(+) ( Q .(+) R ) ) = ( U .(+) ( R .(+) Q ) ) )
        31 25 5 sseldd
         |-  ( ph -> U e. ( SubGrp ` W ) )
        32 2 lsmass
         |-  ( ( U e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) /\ Q e. ( SubGrp ` W ) ) -> ( ( U .(+) R ) .(+) Q ) = ( U .(+) ( R .(+) Q ) ) )
        33 31 27 26 32 syl3anc
         |-  ( ph -> ( ( U .(+) R ) .(+) Q ) = ( U .(+) ( R .(+) Q ) ) )
        34 30 33 eqtr4d
         |-  ( ph -> ( U .(+) ( Q .(+) R ) ) = ( ( U .(+) R ) .(+) Q ) )
        35 1 2 lsmcl
         |-  ( ( W e. LMod /\ U e. S /\ R e. S ) -> ( U .(+) R ) e. S )
        36 13 5 15 35 syl3anc
         |-  ( ph -> ( U .(+) R ) e. S )
        37 25 36 sseldd
         |-  ( ph -> ( U .(+) R ) e. ( SubGrp ` W ) )
        38 2 lsmless2
         |-  ( ( ( U .(+) R ) e. ( SubGrp ` W ) /\ ( U .(+) R ) e. ( SubGrp ` W ) /\ Q C_ ( U .(+) R ) ) -> ( ( U .(+) R ) .(+) Q ) C_ ( ( U .(+) R ) .(+) ( U .(+) R ) ) )
        39 37 37 10 38 syl3anc
         |-  ( ph -> ( ( U .(+) R ) .(+) Q ) C_ ( ( U .(+) R ) .(+) ( U .(+) R ) ) )
        40 34 39 eqsstrd
         |-  ( ph -> ( U .(+) ( Q .(+) R ) ) C_ ( ( U .(+) R ) .(+) ( U .(+) R ) ) )
        41 2 lsmidm
         |-  ( ( U .(+) R ) e. ( SubGrp ` W ) -> ( ( U .(+) R ) .(+) ( U .(+) R ) ) = ( U .(+) R ) )
        42 37 41 syl
         |-  ( ph -> ( ( U .(+) R ) .(+) ( U .(+) R ) ) = ( U .(+) R ) )
        43 40 42 sseqtrd
         |-  ( ph -> ( U .(+) ( Q .(+) R ) ) C_ ( U .(+) R ) )
        44 25 17 sseldd
         |-  ( ph -> ( Q .(+) R ) e. ( SubGrp ` W ) )
        45 2 lsmub2
         |-  ( ( Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> R C_ ( Q .(+) R ) )
        46 26 27 45 syl2anc
         |-  ( ph -> R C_ ( Q .(+) R ) )
        47 2 lsmless2
         |-  ( ( U e. ( SubGrp ` W ) /\ ( Q .(+) R ) e. ( SubGrp ` W ) /\ R C_ ( Q .(+) R ) ) -> ( U .(+) R ) C_ ( U .(+) ( Q .(+) R ) ) )
        48 31 44 46 47 syl3anc
         |-  ( ph -> ( U .(+) R ) C_ ( U .(+) ( Q .(+) R ) ) )
        49 43 48 eqssd
         |-  ( ph -> ( U .(+) ( Q .(+) R ) ) = ( U .(+) R ) )
        50 21 49 breqtrrd
         |-  ( ph -> U ( 
          51 1 2 11 13 5 17 50 lcvexchlem4
           |-  ( ph -> ( U i^i ( Q .(+) R ) ) ( 
            52 1 2 3 11 4 19 6 7 8 51 lsatcvat2
             |-  ( ph -> ( U i^i ( Q .(+) R ) ) e. A )