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𝑊 )
lsatcvat.s 𝑆 = ( LSubSp ‘ 𝑊 )
lsatcvat.p = ( LSSum ‘ 𝑊 )
lsatcvat.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcvat.w ( 𝜑𝑊 ∈ LVec )
lsatcvat.u ( 𝜑𝑈𝑆 )
lsatcvat.q ( 𝜑𝑄𝐴 )
lsatcvat.r ( 𝜑𝑅𝐴 )
lsatcvat.n ( 𝜑𝑈 ≠ { 0 } )
lsatcvat.l ( 𝜑𝑈 ⊊ ( 𝑄 𝑅 ) )
Assertion lsatcvat ( 𝜑𝑈𝐴 )

Proof

Step Hyp Ref Expression
1 lsatcvat.o 0 = ( 0g𝑊 )
2 lsatcvat.s 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsatcvat.p = ( LSSum ‘ 𝑊 )
4 lsatcvat.a 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsatcvat.w ( 𝜑𝑊 ∈ LVec )
6 lsatcvat.u ( 𝜑𝑈𝑆 )
7 lsatcvat.q ( 𝜑𝑄𝐴 )
8 lsatcvat.r ( 𝜑𝑅𝐴 )
9 lsatcvat.n ( 𝜑𝑈 ≠ { 0 } )
10 lsatcvat.l ( 𝜑𝑈 ⊊ ( 𝑄 𝑅 ) )
11 5 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑊 ∈ LVec )
12 6 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑈𝑆 )
13 7 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑄𝐴 )
14 8 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑅𝐴 )
15 9 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑈 ≠ { 0 } )
16 10 adantr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑈 ⊊ ( 𝑄 𝑅 ) )
17 simpr ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → ¬ 𝑄𝑈 )
18 1 2 3 4 11 12 13 14 15 16 17 lsatcvatlem ( ( 𝜑 ∧ ¬ 𝑄𝑈 ) → 𝑈𝐴 )
19 5 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑊 ∈ LVec )
20 6 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑈𝑆 )
21 8 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑅𝐴 )
22 7 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑄𝐴 )
23 9 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑈 ≠ { 0 } )
24 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25 5 24 syl ( 𝜑𝑊 ∈ LMod )
26 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
27 25 26 syl ( 𝜑𝑊 ∈ Abel )
28 2 lsssssubg ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
29 25 28 syl ( 𝜑𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
30 2 4 25 7 lsatlssel ( 𝜑𝑄𝑆 )
31 29 30 sseldd ( 𝜑𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
32 2 4 25 8 lsatlssel ( 𝜑𝑅𝑆 )
33 29 32 sseldd ( 𝜑𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
34 3 lsmcom ( ( 𝑊 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
35 27 31 33 34 syl3anc ( 𝜑 → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
36 35 psseq2d ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 𝑅 ) ↔ 𝑈 ⊊ ( 𝑅 𝑄 ) ) )
37 10 36 mpbid ( 𝜑𝑈 ⊊ ( 𝑅 𝑄 ) )
38 37 adantr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑈 ⊊ ( 𝑅 𝑄 ) )
39 simpr ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → ¬ 𝑅𝑈 )
40 1 2 3 4 19 20 21 22 23 38 39 lsatcvatlem ( ( 𝜑 ∧ ¬ 𝑅𝑈 ) → 𝑈𝐴 )
41 29 6 sseldd ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
42 3 lsmlub ( ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑄𝑈𝑅𝑈 ) ↔ ( 𝑄 𝑅 ) ⊆ 𝑈 ) )
43 31 33 41 42 syl3anc ( 𝜑 → ( ( 𝑄𝑈𝑅𝑈 ) ↔ ( 𝑄 𝑅 ) ⊆ 𝑈 ) )
44 ssnpss ( ( 𝑄 𝑅 ) ⊆ 𝑈 → ¬ 𝑈 ⊊ ( 𝑄 𝑅 ) )
45 43 44 syl6bi ( 𝜑 → ( ( 𝑄𝑈𝑅𝑈 ) → ¬ 𝑈 ⊊ ( 𝑄 𝑅 ) ) )
46 45 con2d ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 𝑅 ) → ¬ ( 𝑄𝑈𝑅𝑈 ) ) )
47 ianor ( ¬ ( 𝑄𝑈𝑅𝑈 ) ↔ ( ¬ 𝑄𝑈 ∨ ¬ 𝑅𝑈 ) )
48 46 47 syl6ib ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 𝑅 ) → ( ¬ 𝑄𝑈 ∨ ¬ 𝑅𝑈 ) ) )
49 10 48 mpd ( 𝜑 → ( ¬ 𝑄𝑈 ∨ ¬ 𝑅𝑈 ) )
50 18 40 49 mpjaodan ( 𝜑𝑈𝐴 )