Metamath Proof Explorer


Theorem lsatcvat

Description: A nonzero subspace less than the sum of two atoms is an atom. ( atcvati analog.) (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 ) )
Assertion lsatcvat
|- ( 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 5 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> W e. LVec )
12 6 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> U e. S )
13 7 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> Q e. A )
14 8 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> R e. A )
15 9 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> U =/= { .0. } )
16 10 adantr
 |-  ( ( ph /\ -. Q C_ U ) -> U C. ( Q .(+) R ) )
17 simpr
 |-  ( ( ph /\ -. Q C_ U ) -> -. Q C_ U )
18 1 2 3 4 11 12 13 14 15 16 17 lsatcvatlem
 |-  ( ( ph /\ -. Q C_ U ) -> U e. A )
19 5 adantr
 |-  ( ( ph /\ -. R C_ U ) -> W e. LVec )
20 6 adantr
 |-  ( ( ph /\ -. R C_ U ) -> U e. S )
21 8 adantr
 |-  ( ( ph /\ -. R C_ U ) -> R e. A )
22 7 adantr
 |-  ( ( ph /\ -. R C_ U ) -> Q e. A )
23 9 adantr
 |-  ( ( ph /\ -. R C_ U ) -> U =/= { .0. } )
24 lveclmod
 |-  ( W e. LVec -> W e. LMod )
25 5 24 syl
 |-  ( ph -> W e. LMod )
26 lmodabl
 |-  ( W e. LMod -> W e. Abel )
27 25 26 syl
 |-  ( ph -> W e. Abel )
28 2 lsssssubg
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
29 25 28 syl
 |-  ( ph -> S C_ ( SubGrp ` W ) )
30 2 4 25 7 lsatlssel
 |-  ( ph -> Q e. S )
31 29 30 sseldd
 |-  ( ph -> Q e. ( SubGrp ` W ) )
32 2 4 25 8 lsatlssel
 |-  ( ph -> R e. S )
33 29 32 sseldd
 |-  ( ph -> R e. ( SubGrp ` W ) )
34 3 lsmcom
 |-  ( ( W e. Abel /\ Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> ( Q .(+) R ) = ( R .(+) Q ) )
35 27 31 33 34 syl3anc
 |-  ( ph -> ( Q .(+) R ) = ( R .(+) Q ) )
36 35 psseq2d
 |-  ( ph -> ( U C. ( Q .(+) R ) <-> U C. ( R .(+) Q ) ) )
37 10 36 mpbid
 |-  ( ph -> U C. ( R .(+) Q ) )
38 37 adantr
 |-  ( ( ph /\ -. R C_ U ) -> U C. ( R .(+) Q ) )
39 simpr
 |-  ( ( ph /\ -. R C_ U ) -> -. R C_ U )
40 1 2 3 4 19 20 21 22 23 38 39 lsatcvatlem
 |-  ( ( ph /\ -. R C_ U ) -> U e. A )
41 29 6 sseldd
 |-  ( ph -> U e. ( SubGrp ` W ) )
42 3 lsmlub
 |-  ( ( Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( ( Q C_ U /\ R C_ U ) <-> ( Q .(+) R ) C_ U ) )
43 31 33 41 42 syl3anc
 |-  ( ph -> ( ( Q C_ U /\ R C_ U ) <-> ( Q .(+) R ) C_ U ) )
44 ssnpss
 |-  ( ( Q .(+) R ) C_ U -> -. U C. ( Q .(+) R ) )
45 43 44 syl6bi
 |-  ( ph -> ( ( Q C_ U /\ R C_ U ) -> -. U C. ( Q .(+) R ) ) )
46 45 con2d
 |-  ( ph -> ( U C. ( Q .(+) R ) -> -. ( Q C_ U /\ R C_ U ) ) )
47 ianor
 |-  ( -. ( Q C_ U /\ R C_ U ) <-> ( -. Q C_ U \/ -. R C_ U ) )
48 46 47 syl6ib
 |-  ( ph -> ( U C. ( Q .(+) R ) -> ( -. Q C_ U \/ -. R C_ U ) ) )
49 10 48 mpd
 |-  ( ph -> ( -. Q C_ U \/ -. R C_ U ) )
50 18 40 49 mpjaodan
 |-  ( ph -> U e. A )