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 |
|
dalem59.m |
|- ./\ = ( meet ` K ) |
7 |
|
dalem59.o |
|- O = ( LPlanes ` K ) |
8 |
|
dalem59.y |
|- Y = ( ( P .\/ Q ) .\/ R ) |
9 |
|
dalem59.z |
|- Z = ( ( S .\/ T ) .\/ U ) |
10 |
|
dalem59.f |
|- F = ( ( R .\/ P ) ./\ ( U .\/ S ) ) |
11 |
|
dalem59.g |
|- G = ( ( c .\/ P ) ./\ ( d .\/ S ) ) |
12 |
|
dalem59.h |
|- H = ( ( c .\/ Q ) ./\ ( d .\/ T ) ) |
13 |
|
dalem59.i |
|- I = ( ( c .\/ R ) ./\ ( d .\/ U ) ) |
14 |
|
dalem59.b1 |
|- B = ( ( ( G .\/ H ) .\/ I ) ./\ Y ) |
15 |
1 2 3 4 8 9
|
dalemrot |
|- ( ph -> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) ) |
16 |
15
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) ) |
17 |
1 2 3 4 8 9
|
dalemrotyz |
|- ( ( ph /\ Y = Z ) -> ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) ) |
18 |
17
|
3adant3 |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) ) |
19 |
1 2 3 4 5 8
|
dalemrotps |
|- ( ( ph /\ ps ) -> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) ) |
20 |
19
|
3adant2 |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) ) |
21 |
|
biid |
|- ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) ) |
22 |
|
biid |
|- ( ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) ) |
23 |
|
eqid |
|- ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ P ) |
24 |
|
eqid |
|- ( ( T .\/ U ) .\/ S ) = ( ( T .\/ U ) .\/ S ) |
25 |
|
eqid |
|- ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) = ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) |
26 |
21 2 3 4 22 6 7 23 24 10 12 13 11 25
|
dalem58 |
|- ( ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) /\ ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) /\ ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) ) -> F .<_ ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) ) |
27 |
16 18 20 26
|
syl3anc |
|- ( ( ph /\ Y = Z /\ ps ) -> F .<_ ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) ) |
28 |
1
|
dalemkehl |
|- ( ph -> K e. HL ) |
29 |
28
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> K e. HL ) |
30 |
1 2 3 4 5 6 7 8 9 12
|
dalem29 |
|- ( ( ph /\ Y = Z /\ ps ) -> H e. A ) |
31 |
1 2 3 4 5 6 7 8 9 13
|
dalem34 |
|- ( ( ph /\ Y = Z /\ ps ) -> I e. A ) |
32 |
1 2 3 4 5 6 7 8 9 11
|
dalem23 |
|- ( ( ph /\ Y = Z /\ ps ) -> G e. A ) |
33 |
3 4
|
hlatjrot |
|- ( ( K e. HL /\ ( H e. A /\ I e. A /\ G e. A ) ) -> ( ( H .\/ I ) .\/ G ) = ( ( G .\/ H ) .\/ I ) ) |
34 |
29 30 31 32 33
|
syl13anc |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( H .\/ I ) .\/ G ) = ( ( G .\/ H ) .\/ I ) ) |
35 |
1 3 4
|
dalemqrprot |
|- ( ph -> ( ( Q .\/ R ) .\/ P ) = ( ( P .\/ Q ) .\/ R ) ) |
36 |
35 8
|
eqtr4di |
|- ( ph -> ( ( Q .\/ R ) .\/ P ) = Y ) |
37 |
36
|
3ad2ant1 |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( Q .\/ R ) .\/ P ) = Y ) |
38 |
34 37
|
oveq12d |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) = ( ( ( G .\/ H ) .\/ I ) ./\ Y ) ) |
39 |
38 14
|
eqtr4di |
|- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( H .\/ I ) .\/ G ) ./\ ( ( Q .\/ R ) .\/ P ) ) = B ) |
40 |
27 39
|
breqtrd |
|- ( ( ph /\ Y = Z /\ ps ) -> F .<_ B ) |