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 )