Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemf.l |
|- .<_ = ( le ` K ) |
2 |
|
cdlemf.a |
|- A = ( Atoms ` K ) |
3 |
|
cdlemf.h |
|- H = ( LHyp ` K ) |
4 |
|
cdlemf.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
cdlemf.r |
|- R = ( ( trL ` K ) ` W ) |
6 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
7 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
8 |
1 6 2 3 7
|
cdlemf2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) |
9 |
|
simp1l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( K e. HL /\ W e. H ) ) |
10 |
|
simp2l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> p e. A ) |
11 |
|
simp3ll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> -. p .<_ W ) |
12 |
|
simp2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> q e. A ) |
13 |
|
simp3lr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> -. q .<_ W ) |
14 |
1 2 3 4
|
cdleme50ex |
|- ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ -. p .<_ W ) /\ ( q e. A /\ -. q .<_ W ) ) -> E. f e. T ( f ` p ) = q ) |
15 |
9 10 11 12 13 14
|
syl122anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> E. f e. T ( f ` p ) = q ) |
16 |
|
simp3r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( f ` p ) = q ) |
17 |
16
|
oveq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( p ( join ` K ) ( f ` p ) ) = ( p ( join ` K ) q ) ) |
18 |
17
|
oveq1d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) |
19 |
|
simp11 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( K e. HL /\ W e. H ) ) |
20 |
|
simp3l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> f e. T ) |
21 |
|
simp13l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> p e. A ) |
22 |
|
simp2ll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> -. p .<_ W ) |
23 |
1 6 7 2 3 4 5
|
trlval2 |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ ( p e. A /\ -. p .<_ W ) ) -> ( R ` f ) = ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) ) |
24 |
19 20 21 22 23
|
syl112anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( R ` f ) = ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) ) |
25 |
|
simp2r |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) |
26 |
18 24 25
|
3eqtr4d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( R ` f ) = U ) |
27 |
26
|
3exp |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) ) ) |
28 |
27
|
3expia |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ q e. A ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) ) ) ) |
29 |
28
|
3imp |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) ) |
30 |
29
|
expd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( f e. T -> ( ( f ` p ) = q -> ( R ` f ) = U ) ) ) |
31 |
30
|
reximdvai |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( E. f e. T ( f ` p ) = q -> E. f e. T ( R ` f ) = U ) ) |
32 |
15 31
|
mpd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> E. f e. T ( R ` f ) = U ) |
33 |
32
|
3exp |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ q e. A ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> E. f e. T ( R ` f ) = U ) ) ) |
34 |
33
|
rexlimdvv |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> E. f e. T ( R ` f ) = U ) ) |
35 |
8 34
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. f e. T ( R ` f ) = U ) |