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 biimtrdi 
 |-  ( 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 imbitrdi 
 |-  ( 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 )