Step |
Hyp |
Ref |
Expression |
1 |
|
dalema.ph |
|- ( ph <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) ) |
2 |
|
dalemc.l |
|- .<_ = ( le ` K ) |
3 |
|
dalemc.j |
|- .\/ = ( join ` K ) |
4 |
|
dalemc.a |
|- A = ( Atoms ` K ) |
5 |
|
dalem5.o |
|- O = ( LPlanes ` K ) |
6 |
|
dalem5.y |
|- Y = ( ( P .\/ Q ) .\/ R ) |
7 |
|
dalem5.w |
|- W = ( Y .\/ C ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
1
|
dalemkelat |
|- ( ph -> K e. Lat ) |
10 |
1 4
|
dalemueb |
|- ( ph -> U e. ( Base ` K ) ) |
11 |
1
|
dalemkehl |
|- ( ph -> K e. HL ) |
12 |
1
|
dalemrea |
|- ( ph -> R e. A ) |
13 |
1 2 3 4 5 6
|
dalemcea |
|- ( ph -> C e. A ) |
14 |
8 3 4
|
hlatjcl |
|- ( ( K e. HL /\ R e. A /\ C e. A ) -> ( R .\/ C ) e. ( Base ` K ) ) |
15 |
11 12 13 14
|
syl3anc |
|- ( ph -> ( R .\/ C ) e. ( Base ` K ) ) |
16 |
1 5
|
dalemyeb |
|- ( ph -> Y e. ( Base ` K ) ) |
17 |
1 4
|
dalemceb |
|- ( ph -> C e. ( Base ` K ) ) |
18 |
8 3
|
latjcl |
|- ( ( K e. Lat /\ Y e. ( Base ` K ) /\ C e. ( Base ` K ) ) -> ( Y .\/ C ) e. ( Base ` K ) ) |
19 |
9 16 17 18
|
syl3anc |
|- ( ph -> ( Y .\/ C ) e. ( Base ` K ) ) |
20 |
7 19
|
eqeltrid |
|- ( ph -> W e. ( Base ` K ) ) |
21 |
1
|
dalemclrju |
|- ( ph -> C .<_ ( R .\/ U ) ) |
22 |
1
|
dalemuea |
|- ( ph -> U e. A ) |
23 |
1
|
dalempea |
|- ( ph -> P e. A ) |
24 |
|
simp313 |
|- ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) /\ ( Y e. O /\ Z e. O ) /\ ( ( -. C .<_ ( P .\/ Q ) /\ -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) ) /\ ( -. C .<_ ( S .\/ T ) /\ -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) ) /\ ( C .<_ ( P .\/ S ) /\ C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) ) ) ) -> -. C .<_ ( R .\/ P ) ) |
25 |
1 24
|
sylbi |
|- ( ph -> -. C .<_ ( R .\/ P ) ) |
26 |
2 3 4
|
atnlej1 |
|- ( ( K e. HL /\ ( C e. A /\ R e. A /\ P e. A ) /\ -. C .<_ ( R .\/ P ) ) -> C =/= R ) |
27 |
11 13 12 23 25 26
|
syl131anc |
|- ( ph -> C =/= R ) |
28 |
2 3 4
|
hlatexch1 |
|- ( ( K e. HL /\ ( C e. A /\ U e. A /\ R e. A ) /\ C =/= R ) -> ( C .<_ ( R .\/ U ) -> U .<_ ( R .\/ C ) ) ) |
29 |
11 13 22 12 27 28
|
syl131anc |
|- ( ph -> ( C .<_ ( R .\/ U ) -> U .<_ ( R .\/ C ) ) ) |
30 |
21 29
|
mpd |
|- ( ph -> U .<_ ( R .\/ C ) ) |
31 |
1 3 4
|
dalempjqeb |
|- ( ph -> ( P .\/ Q ) e. ( Base ` K ) ) |
32 |
1 4
|
dalemreb |
|- ( ph -> R e. ( Base ` K ) ) |
33 |
8 2 3
|
latlej2 |
|- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> R .<_ ( ( P .\/ Q ) .\/ R ) ) |
34 |
9 31 32 33
|
syl3anc |
|- ( ph -> R .<_ ( ( P .\/ Q ) .\/ R ) ) |
35 |
34 6
|
breqtrrdi |
|- ( ph -> R .<_ Y ) |
36 |
8 2 3
|
latjlej1 |
|- ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ C e. ( Base ` K ) ) ) -> ( R .<_ Y -> ( R .\/ C ) .<_ ( Y .\/ C ) ) ) |
37 |
9 32 16 17 36
|
syl13anc |
|- ( ph -> ( R .<_ Y -> ( R .\/ C ) .<_ ( Y .\/ C ) ) ) |
38 |
35 37
|
mpd |
|- ( ph -> ( R .\/ C ) .<_ ( Y .\/ C ) ) |
39 |
38 7
|
breqtrrdi |
|- ( ph -> ( R .\/ C ) .<_ W ) |
40 |
8 2 9 10 15 20 30 39
|
lattrd |
|- ( ph -> U .<_ W ) |