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 biimtrdi ⊢ ( 𝜑 → ( ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) → ¬ 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) ) )
46 45 con2d ⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) → ¬ ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ) )
47 ianor ⊢ ( ¬ ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ↔ ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) )
48 46 47 imbitrdi ⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) → ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) ) )
49 10 48 mpd ⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) )
50 18 40 49 mpjaodan ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )