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 syl5bb φ 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