This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> W e. LMod )
lrelat.t 
|- ( ph -> T e. S )
lrelat.u 
|- ( ph -> U e. S )
lrelat.l 
|- ( ph -> T C. U )
Assertion lrelat 
|- ( ph -> E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ 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 
 |-  ( ph -> W e. LMod )
5 lrelat.t 
 |-  ( ph -> T e. S )
6 lrelat.u 
 |-  ( ph -> U e. S )
7 lrelat.l 
 |-  ( ph -> T C. U )
8 1 3 4 5 6 7 lpssat 
 |-  ( ph -> E. q e. A ( q C_ U /\ -. q C_ T ) )
9 ancom 
 |-  ( ( q C_ U /\ -. q C_ T ) <-> ( -. q C_ T /\ q C_ U ) )
10 4 adantr 
 |-  ( ( ph /\ q e. A ) -> W e. LMod )
11 1 lsssssubg 
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
12 10 11 syl 
 |-  ( ( ph /\ q e. A ) -> S C_ ( SubGrp ` W ) )
13 5 adantr 
 |-  ( ( ph /\ q e. A ) -> T e. S )
14 12 13 sseldd 
 |-  ( ( ph /\ q e. A ) -> T e. ( SubGrp ` W ) )
15 simpr 
 |-  ( ( ph /\ q e. A ) -> q e. A )
16 1 3 10 15 lsatlssel 
 |-  ( ( ph /\ q e. A ) -> q e. S )
17 12 16 sseldd 
 |-  ( ( ph /\ q e. A ) -> q e. ( SubGrp ` W ) )
18 2 14 17 lssnle 
 |-  ( ( ph /\ q e. A ) -> ( -. q C_ T <-> T C. ( T .(+) q ) ) )
19 7 pssssd 
 |-  ( ph -> T C_ U )
20 19 adantr 
 |-  ( ( ph /\ q e. A ) -> T C_ U )
21 20 biantrurd 
 |-  ( ( ph /\ q e. A ) -> ( q C_ U <-> ( T C_ U /\ q C_ U ) ) )
22 6 adantr 
 |-  ( ( ph /\ q e. A ) -> U e. S )
23 12 22 sseldd 
 |-  ( ( ph /\ q e. A ) -> U e. ( SubGrp ` W ) )
24 2 lsmlub 
 |-  ( ( T e. ( SubGrp ` W ) /\ q e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( ( T C_ U /\ q C_ U ) <-> ( T .(+) q ) C_ U ) )
25 14 17 23 24 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( ( T C_ U /\ q C_ U ) <-> ( T .(+) q ) C_ U ) )
26 21 25 bitrd 
 |-  ( ( ph /\ q e. A ) -> ( q C_ U <-> ( T .(+) q ) C_ U ) )
27 18 26 anbi12d 
 |-  ( ( ph /\ q e. A ) -> ( ( -. q C_ T /\ q C_ U ) <-> ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) )
28 9 27 bitrid 
 |-  ( ( ph /\ q e. A ) -> ( ( q C_ U /\ -. q C_ T ) <-> ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) )
29 28 rexbidva 
 |-  ( ph -> ( E. q e. A ( q C_ U /\ -. q C_ T ) <-> E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) )
30 8 29 mpbid 
 |-  ( ph -> E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) )