Step |
Hyp |
Ref |
Expression |
1 |
|
dalem.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 |
|
dalem.l |
|- .<_ = ( le ` K ) |
3 |
|
dalem.j |
|- .\/ = ( join ` K ) |
4 |
|
dalem.a |
|- A = ( Atoms ` K ) |
5 |
|
dalem.ps |
|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) ) |
6 |
|
dalem23.m |
|- ./\ = ( meet ` K ) |
7 |
|
dalem23.o |
|- O = ( LPlanes ` K ) |
8 |
|
dalem23.y |
|- Y = ( ( P .\/ Q ) .\/ R ) |
9 |
|
dalem23.z |
|- Z = ( ( S .\/ T ) .\/ U ) |
10 |
|
dalem23.g |
|- G = ( ( c .\/ P ) ./\ ( d .\/ S ) ) |
11 |
1 2 3 4
|
dalemcnes |
|- ( ph -> C =/= S ) |
12 |
11
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> C =/= S ) |
13 |
5
|
dalemclccjdd |
|- ( ps -> C .<_ ( c .\/ d ) ) |
14 |
13
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> C .<_ ( c .\/ d ) ) |
15 |
14
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> C .<_ ( c .\/ d ) ) |
16 |
|
simpr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> c = G ) |
17 |
1
|
dalemkelat |
|- ( ph -> K e. Lat ) |
18 |
17
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> K e. Lat ) |
19 |
1
|
dalemkehl |
|- ( ph -> K e. HL ) |
20 |
19
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> K e. HL ) |
21 |
5
|
dalemccea |
|- ( ps -> c e. A ) |
22 |
21
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> c e. A ) |
23 |
1
|
dalempea |
|- ( ph -> P e. A ) |
24 |
23
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> P e. A ) |
25 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
26 |
25 3 4
|
hlatjcl |
|- ( ( K e. HL /\ c e. A /\ P e. A ) -> ( c .\/ P ) e. ( Base ` K ) ) |
27 |
20 22 24 26
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( c .\/ P ) e. ( Base ` K ) ) |
28 |
5
|
dalemddea |
|- ( ps -> d e. A ) |
29 |
28
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> d e. A ) |
30 |
1
|
dalemsea |
|- ( ph -> S e. A ) |
31 |
30
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> S e. A ) |
32 |
25 3 4
|
hlatjcl |
|- ( ( K e. HL /\ d e. A /\ S e. A ) -> ( d .\/ S ) e. ( Base ` K ) ) |
33 |
20 29 31 32
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( d .\/ S ) e. ( Base ` K ) ) |
34 |
25 2 6
|
latmle2 |
|- ( ( K e. Lat /\ ( c .\/ P ) e. ( Base ` K ) /\ ( d .\/ S ) e. ( Base ` K ) ) -> ( ( c .\/ P ) ./\ ( d .\/ S ) ) .<_ ( d .\/ S ) ) |
35 |
18 27 33 34
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( c .\/ P ) ./\ ( d .\/ S ) ) .<_ ( d .\/ S ) ) |
36 |
10 35
|
eqbrtrid |
|- ( ( ph /\ Y = Z /\ ps ) -> G .<_ ( d .\/ S ) ) |
37 |
3 4
|
hlatjcom |
|- ( ( K e. HL /\ d e. A /\ S e. A ) -> ( d .\/ S ) = ( S .\/ d ) ) |
38 |
20 29 31 37
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( d .\/ S ) = ( S .\/ d ) ) |
39 |
36 38
|
breqtrd |
|- ( ( ph /\ Y = Z /\ ps ) -> G .<_ ( S .\/ d ) ) |
40 |
39
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> G .<_ ( S .\/ d ) ) |
41 |
16 40
|
eqbrtrd |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> c .<_ ( S .\/ d ) ) |
42 |
2 3 4
|
hlatlej2 |
|- ( ( K e. HL /\ S e. A /\ d e. A ) -> d .<_ ( S .\/ d ) ) |
43 |
20 31 29 42
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> d .<_ ( S .\/ d ) ) |
44 |
43
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> d .<_ ( S .\/ d ) ) |
45 |
5 4
|
dalemcceb |
|- ( ps -> c e. ( Base ` K ) ) |
46 |
45
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> c e. ( Base ` K ) ) |
47 |
25 4
|
atbase |
|- ( d e. A -> d e. ( Base ` K ) ) |
48 |
28 47
|
syl |
|- ( ps -> d e. ( Base ` K ) ) |
49 |
48
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> d e. ( Base ` K ) ) |
50 |
25 3 4
|
hlatjcl |
|- ( ( K e. HL /\ S e. A /\ d e. A ) -> ( S .\/ d ) e. ( Base ` K ) ) |
51 |
20 31 29 50
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( S .\/ d ) e. ( Base ` K ) ) |
52 |
25 2 3
|
latjle12 |
|- ( ( K e. Lat /\ ( c e. ( Base ` K ) /\ d e. ( Base ` K ) /\ ( S .\/ d ) e. ( Base ` K ) ) ) -> ( ( c .<_ ( S .\/ d ) /\ d .<_ ( S .\/ d ) ) <-> ( c .\/ d ) .<_ ( S .\/ d ) ) ) |
53 |
18 46 49 51 52
|
syl13anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( c .<_ ( S .\/ d ) /\ d .<_ ( S .\/ d ) ) <-> ( c .\/ d ) .<_ ( S .\/ d ) ) ) |
54 |
53
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( ( c .<_ ( S .\/ d ) /\ d .<_ ( S .\/ d ) ) <-> ( c .\/ d ) .<_ ( S .\/ d ) ) ) |
55 |
41 44 54
|
mpbi2and |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( c .\/ d ) .<_ ( S .\/ d ) ) |
56 |
1 4
|
dalemceb |
|- ( ph -> C e. ( Base ` K ) ) |
57 |
56
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> C e. ( Base ` K ) ) |
58 |
25 3 4
|
hlatjcl |
|- ( ( K e. HL /\ c e. A /\ d e. A ) -> ( c .\/ d ) e. ( Base ` K ) ) |
59 |
20 22 29 58
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( c .\/ d ) e. ( Base ` K ) ) |
60 |
25 2
|
lattr |
|- ( ( K e. Lat /\ ( C e. ( Base ` K ) /\ ( c .\/ d ) e. ( Base ` K ) /\ ( S .\/ d ) e. ( Base ` K ) ) ) -> ( ( C .<_ ( c .\/ d ) /\ ( c .\/ d ) .<_ ( S .\/ d ) ) -> C .<_ ( S .\/ d ) ) ) |
61 |
18 57 59 51 60
|
syl13anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( C .<_ ( c .\/ d ) /\ ( c .\/ d ) .<_ ( S .\/ d ) ) -> C .<_ ( S .\/ d ) ) ) |
62 |
61
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( ( C .<_ ( c .\/ d ) /\ ( c .\/ d ) .<_ ( S .\/ d ) ) -> C .<_ ( S .\/ d ) ) ) |
63 |
15 55 62
|
mp2and |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> C .<_ ( S .\/ d ) ) |
64 |
1 7
|
dalemyeb |
|- ( ph -> Y e. ( Base ` K ) ) |
65 |
64
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> Y e. ( Base ` K ) ) |
66 |
25 2 6
|
latmlem1 |
|- ( ( K e. Lat /\ ( C e. ( Base ` K ) /\ ( S .\/ d ) e. ( Base ` K ) /\ Y e. ( Base ` K ) ) ) -> ( C .<_ ( S .\/ d ) -> ( C ./\ Y ) .<_ ( ( S .\/ d ) ./\ Y ) ) ) |
67 |
18 57 51 65 66
|
syl13anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( C .<_ ( S .\/ d ) -> ( C ./\ Y ) .<_ ( ( S .\/ d ) ./\ Y ) ) ) |
68 |
67
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( C .<_ ( S .\/ d ) -> ( C ./\ Y ) .<_ ( ( S .\/ d ) ./\ Y ) ) ) |
69 |
63 68
|
mpd |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( C ./\ Y ) .<_ ( ( S .\/ d ) ./\ Y ) ) |
70 |
1 2 3 4 7 8 9
|
dalem17 |
|- ( ( ph /\ Y = Z ) -> C .<_ Y ) |
71 |
70
|
3adant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> C .<_ Y ) |
72 |
25 2 6
|
latleeqm1 |
|- ( ( K e. Lat /\ C e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( C .<_ Y <-> ( C ./\ Y ) = C ) ) |
73 |
18 57 65 72
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( C .<_ Y <-> ( C ./\ Y ) = C ) ) |
74 |
71 73
|
mpbid |
|- ( ( ph /\ Y = Z /\ ps ) -> ( C ./\ Y ) = C ) |
75 |
74
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( C ./\ Y ) = C ) |
76 |
1 2 3 4 9
|
dalemsly |
|- ( ( ph /\ Y = Z ) -> S .<_ Y ) |
77 |
76
|
3adant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> S .<_ Y ) |
78 |
5
|
dalem-ddly |
|- ( ps -> -. d .<_ Y ) |
79 |
78
|
3ad2ant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> -. d .<_ Y ) |
80 |
25 2 3 6 4
|
2atjm |
|- ( ( K e. HL /\ ( S e. A /\ d e. A /\ Y e. ( Base ` K ) ) /\ ( S .<_ Y /\ -. d .<_ Y ) ) -> ( ( S .\/ d ) ./\ Y ) = S ) |
81 |
20 31 29 65 77 79 80
|
syl132anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( S .\/ d ) ./\ Y ) = S ) |
82 |
81
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( ( S .\/ d ) ./\ Y ) = S ) |
83 |
69 75 82
|
3brtr3d |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> C .<_ S ) |
84 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
85 |
19 84
|
syl |
|- ( ph -> K e. AtLat ) |
86 |
1 2 3 4 7 8
|
dalemcea |
|- ( ph -> C e. A ) |
87 |
2 4
|
atcmp |
|- ( ( K e. AtLat /\ C e. A /\ S e. A ) -> ( C .<_ S <-> C = S ) ) |
88 |
85 86 30 87
|
syl3anc |
|- ( ph -> ( C .<_ S <-> C = S ) ) |
89 |
88
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> ( C .<_ S <-> C = S ) ) |
90 |
89
|
adantr |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> ( C .<_ S <-> C = S ) ) |
91 |
83 90
|
mpbid |
|- ( ( ( ph /\ Y = Z /\ ps ) /\ c = G ) -> C = S ) |
92 |
91
|
ex |
|- ( ( ph /\ Y = Z /\ ps ) -> ( c = G -> C = S ) ) |
93 |
92
|
necon3d |
|- ( ( ph /\ Y = Z /\ ps ) -> ( C =/= S -> c =/= G ) ) |
94 |
12 93
|
mpd |
|- ( ( ph /\ Y = Z /\ ps ) -> c =/= G ) |