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 ⊢ S = LSubSp ⁡ W
lrelat.p ⊢ ⊕ ˙ = LSSum ⁡ W
lrelat.a ⊢ A = LSAtoms ⁡ W
lrelat.w ⊢ φ → W ∈ LMod
lrelat.t ⊢ φ → T ∈ S
lrelat.u ⊢ φ → U ∈ S
lrelat.l ⊢ φ → T ⊂ U
Assertion lrelat ⊢ φ → ∃ q ∈ A T ⊂ T ⊕ ˙ q ∧ T ⊕ ˙ q ⊆ U

Proof

Step Hyp Ref Expression
1 lrelat.s ⊢ S = LSubSp ⁡ W
2 lrelat.p ⊢ ⊕ ˙ = LSSum ⁡ W
3 lrelat.a ⊢ A = LSAtoms ⁡ W
4 lrelat.w ⊢ φ → W ∈ LMod
5 lrelat.t ⊢ φ → T ∈ S
6 lrelat.u ⊢ φ → U ∈ S
7 lrelat.l ⊢ φ → T ⊂ U
8 1 3 4 5 6 7 lpssat ⊢ φ → ∃ q ∈ A q ⊆ U ∧ ¬ q ⊆ T
9 ancom ⊢ q ⊆ U ∧ ¬ q ⊆ T ↔ ¬ q ⊆ T ∧ q ⊆ U
10 4 adantr ⊢ φ ∧ q ∈ A → W ∈ LMod
11 1 lsssssubg ⊢ W ∈ LMod → S ⊆ SubGrp ⁡ W
12 10 11 syl ⊢ φ ∧ q ∈ A → S ⊆ SubGrp ⁡ W
13 5 adantr ⊢ φ ∧ q ∈ A → T ∈ S
14 12 13 sseldd ⊢ φ ∧ q ∈ A → T ∈ SubGrp ⁡ W
15 simpr ⊢ φ ∧ q ∈ A → q ∈ A
16 1 3 10 15 lsatlssel ⊢ φ ∧ q ∈ A → q ∈ S
17 12 16 sseldd ⊢ φ ∧ q ∈ A → q ∈ SubGrp ⁡ W
18 2 14 17 lssnle ⊢ φ ∧ q ∈ A → ¬ q ⊆ T ↔ T ⊂ T ⊕ ˙ q
19 7 pssssd ⊢ φ → T ⊆ U
20 19 adantr ⊢ φ ∧ q ∈ A → T ⊆ U
21 20 biantrurd ⊢ φ ∧ q ∈ A → q ⊆ U ↔ T ⊆ U ∧ q ⊆ U
22 6 adantr ⊢ φ ∧ q ∈ A → U ∈ S
23 12 22 sseldd ⊢ φ ∧ q ∈ A → U ∈ SubGrp ⁡ W
24 2 lsmlub ⊢ T ∈ SubGrp ⁡ W ∧ q ∈ SubGrp ⁡ W ∧ U ∈ SubGrp ⁡ W → T ⊆ U ∧ q ⊆ U ↔ T ⊕ ˙ q ⊆ U
25 14 17 23 24 syl3anc ⊢ φ ∧ q ∈ A → T ⊆ U ∧ q ⊆ U ↔ T ⊕ ˙ q ⊆ U
26 21 25 bitrd ⊢ φ ∧ q ∈ A → q ⊆ U ↔ T ⊕ ˙ q ⊆ U
27 18 26 anbi12d ⊢ φ ∧ q ∈ A → ¬ q ⊆ T ∧ q ⊆ U ↔ T ⊂ T ⊕ ˙ q ∧ T ⊕ ˙ q ⊆ U
28 9 27 bitrid ⊢ φ ∧ q ∈ A → q ⊆ U ∧ ¬ q ⊆ T ↔ T ⊂ T ⊕ ˙ q ∧ T ⊕ ˙ q ⊆ U
29 28 rexbidva ⊢ φ → ∃ q ∈ A q ⊆ U ∧ ¬ q ⊆ T ↔ ∃ q ∈ A T ⊂ T ⊕ ˙ q ∧ T ⊕ ˙ q ⊆ U
30 8 29 mpbid ⊢ φ → ∃ q ∈ A T ⊂ T ⊕ ˙ q ∧ T ⊕ ˙ q ⊆ U