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 ) |