Metamath Proof Explorer

Theorem lplncvrlvol2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses lplncvrlvol2.l 
|- .<_ = ( le ` K )
lplncvrlvol2.c 
|- C = (
lplncvrlvol2.p 
|- P = ( LPlanes ` K )
lplncvrlvol2.v 
|- V = ( LVols ` K )
Assertion lplncvrlvol2 
|- ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X C Y )

Proof

Step Hyp Ref Expression
1 lplncvrlvol2.l 
 |-  .<_ = ( le ` K )
2 lplncvrlvol2.c 
 |-  C = (
3 lplncvrlvol2.p 
 |-  P = ( LPlanes ` K )
4 lplncvrlvol2.v 
 |-  V = ( LVols ` K )
5 simpr 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X .<_ Y )
6 simpl1 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> K e. HL )
7 simpl3 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> Y e. V )
8 3 4 lvolnelpln 
 |-  ( ( K e. HL /\ Y e. V ) -> -. Y e. P )
9 6 7 8 syl2anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> -. Y e. P )
10 simpl2 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X e. P )
11 eleq1 
 |-  ( X = Y -> ( X e. P <-> Y e. P ) )
12 10 11 syl5ibcom 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> ( X = Y -> Y e. P ) )
13 12 necon3bd 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> ( -. Y e. P -> X =/= Y ) )
14 9 13 mpd 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X =/= Y )
15 eqid 
 |-  ( lt ` K ) = ( lt ` K )
16 1 15 pltval 
 |-  ( ( K e. HL /\ X e. P /\ Y e. V ) -> ( X ( lt ` K ) Y <-> ( X .<_ Y /\ X =/= Y ) ) )
17 16 adantr 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> ( X ( lt ` K ) Y <-> ( X .<_ Y /\ X =/= Y ) ) )
18 5 14 17 mpbir2and 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X ( lt ` K ) Y )
19 simpl1 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> K e. HL )
20 simpl2 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> X e. P )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 21 3 lplnbase 
 |-  ( X e. P -> X e. ( Base ` K ) )
23 20 22 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> X e. ( Base ` K ) )
24 simpl3 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> Y e. V )
25 21 4 lvolbase 
 |-  ( Y e. V -> Y e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> Y e. ( Base ` K ) )
27 simpr 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> X ( lt ` K ) Y )
28 eqid 
 |-  ( join ` K ) = ( join ` K )
29 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
30 21 1 15 28 2 29 hlrelat3 
 |-  ( ( ( K e. HL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ X ( lt ` K ) Y ) -> E. s e. ( Atoms ` K ) ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) )
31 19 23 26 27 30 syl31anc 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> E. s e. ( Atoms ` K ) ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) )
32 21 1 28 29 4 islvol2 
 |-  ( K e. HL -> ( Y e. V <-> ( Y e. ( Base ` K ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) E. w e. ( Atoms ` K ) ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) ) ) )
33 32 adantr 
 |-  ( ( K e. HL /\ X e. P ) -> ( Y e. V <-> ( Y e. ( Base ` K ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) E. w e. ( Atoms ` K ) ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) ) ) )
34 simpr 
 |-  ( ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) )
35 21 1 28 29 3 islpln2 
 |-  ( K e. HL -> ( X e. P <-> ( X e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) ) )
36 simp3rl 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> X C ( X ( join ` K ) s ) )
37 simp3rr 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( X ( join ` K ) s ) .<_ Y )
38 simp133 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> X = ( ( p ( join ` K ) q ) ( join ` K ) r ) )
39 38 oveq1d 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( X ( join ` K ) s ) = ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) )
40 simp23 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) )
41 37 39 40 3brtr3d 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) .<_ ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) )
42 simp11 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) )
43 simp12 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> r e. ( Atoms ` K ) )
44 simp3l 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> s e. ( Atoms ` K ) )
45 simp21l 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> t e. ( Atoms ` K ) )
46 43 44 45 3jca 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) )
47 simp21r 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> u e. ( Atoms ` K ) )
48 simp22l 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> v e. ( Atoms ` K ) )
49 simp22r 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> w e. ( Atoms ` K ) )
50 47 48 49 3jca 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) )
51 simp131 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> p =/= q )
52 simp132 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> -. r .<_ ( p ( join ` K ) q ) )
53 36 38 39 3brtr3d 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( ( p ( join ` K ) q ) ( join ` K ) r ) C ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) )
54 simp111 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> K e. HL )
55 54 hllatd 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> K e. Lat )
56 21 28 29 hlatjcl 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) )
57 42 56 syl 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) )
58 21 29 atbase 
 |-  ( r e. ( Atoms ` K ) -> r e. ( Base ` K ) )
59 43 58 syl 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> r e. ( Base ` K ) )
60 21 28 latjcl 
 |-  ( ( K e. Lat /\ ( p ( join ` K ) q ) e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( ( p ( join ` K ) q ) ( join ` K ) r ) e. ( Base ` K ) )
61 55 57 59 60 syl3anc 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( ( p ( join ` K ) q ) ( join ` K ) r ) e. ( Base ` K ) )
62 21 1 28 2 29 cvr1 
 |-  ( ( K e. HL /\ ( ( p ( join ` K ) q ) ( join ` K ) r ) e. ( Base ` K ) /\ s e. ( Atoms ` K ) ) -> ( -. s .<_ ( ( p ( join ` K ) q ) ( join ` K ) r ) <-> ( ( p ( join ` K ) q ) ( join ` K ) r ) C ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) ) )
63 54 61 44 62 syl3anc 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( -. s .<_ ( ( p ( join ` K ) q ) ( join ` K ) r ) <-> ( ( p ( join ` K ) q ) ( join ` K ) r ) C ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) ) )
64 53 63 mpbird 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> -. s .<_ ( ( p ( join ` K ) q ) ( join ` K ) r ) )
65 1 28 29 4at2 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ -. s .<_ ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) .<_ ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) <-> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) )
66 42 46 50 51 52 64 65 syl33anc 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) .<_ ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) <-> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) )
67 41 66 mpbid 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) ( join ` K ) s ) = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) )
68 67 39 40 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> ( X ( join ` K ) s ) = Y )
69 36 68 breqtrd 
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) /\ ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) ) -> X C Y )
70 69 3exp 
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> ( ( s e. ( Atoms ` K ) /\ ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) -> X C Y ) ) )
71 70 exp4a 
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) /\ ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) )
72 71 3expd 
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ r e. ( Atoms ` K ) /\ ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) )
73 72 rexlimdv3a 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( E. r e. ( Atoms ` K ) ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
74 73 3expib 
 |-  ( K e. HL -> ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( E. r e. ( Atoms ` K ) ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) ) ) )
75 74 rexlimdvv 
 |-  ( K e. HL -> ( E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
76 75 adantld 
 |-  ( K e. HL -> ( ( X e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( p =/= q /\ -. r .<_ ( p ( join ` K ) q ) /\ X = ( ( p ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
77 35 76 sylbid 
 |-  ( K e. HL -> ( X e. P -> ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
78 77 imp31 
 |-  ( ( ( K e. HL /\ X e. P ) /\ ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) )
79 34 78 syl7 
 |-  ( ( ( K e. HL /\ X e. P ) /\ ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) ) -> ( ( v e. ( Atoms ` K ) /\ w e. ( Atoms ` K ) ) -> ( ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) ) )
80 79 rexlimdvv 
 |-  ( ( ( K e. HL /\ X e. P ) /\ ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) ) -> ( E. v e. ( Atoms ` K ) E. w e. ( Atoms ` K ) ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) )
81 80 rexlimdvva 
 |-  ( ( K e. HL /\ X e. P ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) E. w e. ( Atoms ` K ) ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) )
82 81 adantld 
 |-  ( ( K e. HL /\ X e. P ) -> ( ( Y e. ( Base ` K ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) E. w e. ( Atoms ` K ) ( ( t =/= u /\ -. v .<_ ( t ( join ` K ) u ) /\ -. w .<_ ( ( t ( join ` K ) u ) ( join ` K ) v ) ) /\ Y = ( ( ( t ( join ` K ) u ) ( join ` K ) v ) ( join ` K ) w ) ) ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) )
83 33 82 sylbid 
 |-  ( ( K e. HL /\ X e. P ) -> ( Y e. V -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) ) )
84 83 3impia 
 |-  ( ( K e. HL /\ X e. P /\ Y e. V ) -> ( s e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) ) )
85 84 rexlimdv 
 |-  ( ( K e. HL /\ X e. P /\ Y e. V ) -> ( E. s e. ( Atoms ` K ) ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) -> X C Y ) )
86 85 imp 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ E. s e. ( Atoms ` K ) ( X C ( X ( join ` K ) s ) /\ ( X ( join ` K ) s ) .<_ Y ) ) -> X C Y )
87 31 86 syldan 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X ( lt ` K ) Y ) -> X C Y )
88 18 87 syldan 
 |-  ( ( ( K e. HL /\ X e. P /\ Y e. V ) /\ X .<_ Y ) -> X C Y )