Metamath Proof Explorer

Theorem lsatcvatlem

Description: Lemma for lsatcvat . (Contributed by NM, 10-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lsatcvat.o 
 |-  .0. = ( 0g ` W )
2 lsatcvat.s 
 |-  S = ( LSubSp ` W )
3 lsatcvat.p 
 |-  .(+) = ( LSSum ` W )
4 lsatcvat.a 
 |-  A = ( LSAtoms ` W )
5 lsatcvat.w 
 |-  ( ph -> W e. LVec )
6 lsatcvat.u 
 |-  ( ph -> U e. S )
7 lsatcvat.q 
 |-  ( ph -> Q e. A )
8 lsatcvat.r 
 |-  ( ph -> R e. A )
9 lsatcvat.n 
 |-  ( ph -> U =/= { .0. } )
10 lsatcvat.l 
 |-  ( ph -> U C. ( Q .(+) R ) )
11 lsatcvat.m 
 |-  ( ph -> -. Q C_ U )
12 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
13 5 12 syl 
 |-  ( ph -> W e. LMod )
14 2 1 4 13 6 9 lssatomic 
 |-  ( ph -> E. x e. A x C_ U )
15 eqid 
 |-  (
    16 5 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> W e. LVec )
    17 13 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> W e. LMod )
    18 simp2 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> x e. A )
    19 2 4 17 18 lsatlssel 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> x e. S )
    20 2 4 13 7 lsatlssel 
     |-  ( ph -> Q e. S )
    21 20 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> Q e. S )
    22 2 3 lsmcl 
     |-  ( ( W e. LMod /\ Q e. S /\ x e. S ) -> ( Q .(+) x ) e. S )
    23 17 21 19 22 syl3anc 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( Q .(+) x ) e. S )
    24 6 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> U e. S )
    25 11 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> -. Q C_ U )
    26 sseq1 
     |-  ( x = Q -> ( x C_ U <-> Q C_ U ) )
    27 26 biimpcd 
     |-  ( x C_ U -> ( x = Q -> Q C_ U ) )
    28 27 necon3bd 
     |-  ( x C_ U -> ( -. Q C_ U -> x =/= Q ) )
    29 28 3ad2ant3 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( -. Q C_ U -> x =/= Q ) )
    30 25 29 mpd 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> x =/= Q )
    31 7 3ad2ant1 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> Q e. A )
    32 1 4 16 18 31 lsatnem0 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( x =/= Q <-> ( x i^i Q ) = { .0. } ) )
    33 30 32 mpbid 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( x i^i Q ) = { .0. } )
    34 2 3 1 4 15 16 19 31 lcvp 
     |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( ( x i^i Q ) = { .0. } <-> x (
      35 33 34 mpbid 
       |-  ( ( ph /\ x e. A /\ x C_ U ) -> x (
        36 lmodabl 
         |-  ( W e. LMod -> W e. Abel )
        37 17 36 syl 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> W e. Abel )
        38 2 lsssssubg 
         |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
        39 17 38 syl 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> S C_ ( SubGrp ` W ) )
        40 39 19 sseldd 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> x e. ( SubGrp ` W ) )
        41 39 21 sseldd 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> Q e. ( SubGrp ` W ) )
        42 3 lsmcom 
         |-  ( ( W e. Abel /\ x e. ( SubGrp ` W ) /\ Q e. ( SubGrp ` W ) ) -> ( x .(+) Q ) = ( Q .(+) x ) )
        43 37 40 41 42 syl3anc 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( x .(+) Q ) = ( Q .(+) x ) )
        44 35 43 breqtrd 
         |-  ( ( ph /\ x e. A /\ x C_ U ) -> x (
          45 simp3 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> x C_ U )
          46 10 3ad2ant1 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> U C. ( Q .(+) R ) )
          47 3 lsmub1 
           |-  ( ( Q e. ( SubGrp ` W ) /\ x e. ( SubGrp ` W ) ) -> Q C_ ( Q .(+) x ) )
          48 41 40 47 syl2anc 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> Q C_ ( Q .(+) x ) )
          49 8 3ad2ant1 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> R e. A )
          50 10 pssssd 
           |-  ( ph -> U C_ ( Q .(+) R ) )
          51 50 3ad2ant1 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> U C_ ( Q .(+) R ) )
          52 45 51 sstrd 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> x C_ ( Q .(+) R ) )
          53 3 4 16 18 49 31 52 30 lsatexch1 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> R C_ ( Q .(+) x ) )
          54 2 4 13 8 lsatlssel 
           |-  ( ph -> R e. S )
          55 54 3ad2ant1 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> R e. S )
          56 39 55 sseldd 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> R e. ( SubGrp ` W ) )
          57 39 23 sseldd 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( Q .(+) x ) e. ( SubGrp ` W ) )
          58 3 lsmlub 
           |-  ( ( Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) /\ ( Q .(+) x ) e. ( SubGrp ` W ) ) -> ( ( Q C_ ( Q .(+) x ) /\ R C_ ( Q .(+) x ) ) <-> ( Q .(+) R ) C_ ( Q .(+) x ) ) )
          59 41 56 57 58 syl3anc 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( ( Q C_ ( Q .(+) x ) /\ R C_ ( Q .(+) x ) ) <-> ( Q .(+) R ) C_ ( Q .(+) x ) ) )
          60 48 53 59 mpbi2and 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> ( Q .(+) R ) C_ ( Q .(+) x ) )
          61 46 60 psssstrd 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> U C. ( Q .(+) x ) )
          62 2 15 16 19 23 24 44 45 61 lcvnbtwn3 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> U = x )
          63 62 18 eqeltrd 
           |-  ( ( ph /\ x e. A /\ x C_ U ) -> U e. A )
          64 63 rexlimdv3a 
           |-  ( ph -> ( E. x e. A x C_ U -> U e. A ) )
          65 14 64 mpd 
           |-  ( ph -> U e. A )