Metamath Proof Explorer

Theorem lrelat

Description: Subspaces are relatively atomic. Remark 2 of Kalmbach p. 149. ( chrelati analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lrelat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lrelat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lrelat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lrelat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lrelat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lrelat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lrelat.l ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )
Assertion lrelat ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ∧ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lrelat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lrelat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 lrelat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lrelat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lrelat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
6 lrelat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lrelat.l ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )
8 1 3 4 5 6 7 lpssat ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) )
9 ancom ⊢ ( ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) ↔ ( ¬ 𝑞 ⊆ 𝑇 ∧ 𝑞 ⊆ 𝑈 ) )
10 4 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑊 ∈ LMod )
11 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑇 ∈ 𝑆 )
14 12 13 sseldd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
16 1 3 10 15 lsatlssel ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝑆 )
17 12 16 sseldd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ ( SubGrp ‘ 𝑊 ) )
18 2 14 17 lssnle ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ⊆ 𝑇 ↔ 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ) )
19 7 pssssd ⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑇 ⊆ 𝑈 )
21 20 biantrurd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ⊆ 𝑈 ↔ ( 𝑇 ⊆ 𝑈 ∧ 𝑞 ⊆ 𝑈 ) ) )
22 6 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑈 ∈ 𝑆 )
23 12 22 sseldd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
24 2 lsmlub ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑞 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑇 ⊆ 𝑈 ∧ 𝑞 ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) )
25 14 17 23 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑇 ⊆ 𝑈 ∧ 𝑞 ⊆ 𝑈 ) ↔ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) )
26 21 25 bitrd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ⊆ 𝑈 ↔ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) )
27 18 26 anbi12d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑞 ⊆ 𝑇 ∧ 𝑞 ⊆ 𝑈 ) ↔ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ∧ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) ) )
28 9 27 syl5bb ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) ↔ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ∧ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) ) )
29 28 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑞 ∈ 𝐴 ( 𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ∧ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) ) )
30 8 29 mpbid ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑞 ) ∧ ( 𝑇 ⊕ 𝑞 ) ⊆ 𝑈 ) )