Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnel.l |
|- .<_ = ( le ` K ) |
2 |
|
ltrnel.a |
|- A = ( Atoms ` K ) |
3 |
|
ltrnel.h |
|- H = ( LHyp ` K ) |
4 |
|
ltrnel.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
1 2 3 4
|
ltrncnvat |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( `' F ` P ) e. A ) |
6 |
5
|
3adant3r |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( `' F ` P ) e. A ) |
7 |
|
simp3r |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. P .<_ W ) |
8 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) ) |
9 |
|
simp2 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> F e. T ) |
10 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
11 |
10 2
|
atbase |
|- ( ( `' F ` P ) e. A -> ( `' F ` P ) e. ( Base ` K ) ) |
12 |
6 11
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( `' F ` P ) e. ( Base ` K ) ) |
13 |
|
simp1r |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> W e. H ) |
14 |
10 3
|
lhpbase |
|- ( W e. H -> W e. ( Base ` K ) ) |
15 |
13 14
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> W e. ( Base ` K ) ) |
16 |
10 1 3 4
|
ltrnle |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( `' F ` P ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( `' F ` P ) .<_ W <-> ( F ` ( `' F ` P ) ) .<_ ( F ` W ) ) ) |
17 |
8 9 12 15 16
|
syl112anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( `' F ` P ) .<_ W <-> ( F ` ( `' F ` P ) ) .<_ ( F ` W ) ) ) |
18 |
10 3 4
|
ltrn1o |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
19 |
18
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) |
20 |
|
simp3l |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A ) |
21 |
10 2
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
22 |
20 21
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P e. ( Base ` K ) ) |
23 |
|
f1ocnvfv2 |
|- ( ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ P e. ( Base ` K ) ) -> ( F ` ( `' F ` P ) ) = P ) |
24 |
19 22 23
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` ( `' F ` P ) ) = P ) |
25 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL ) |
26 |
25
|
hllatd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> K e. Lat ) |
27 |
10 1
|
latref |
|- ( ( K e. Lat /\ W e. ( Base ` K ) ) -> W .<_ W ) |
28 |
26 15 27
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> W .<_ W ) |
29 |
10 1 3 4
|
ltrnval1 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( W e. ( Base ` K ) /\ W .<_ W ) ) -> ( F ` W ) = W ) |
30 |
8 9 15 28 29
|
syl112anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` W ) = W ) |
31 |
24 30
|
breq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` ( `' F ` P ) ) .<_ ( F ` W ) <-> P .<_ W ) ) |
32 |
17 31
|
bitrd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( `' F ` P ) .<_ W <-> P .<_ W ) ) |
33 |
7 32
|
mtbird |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. ( `' F ` P ) .<_ W ) |
34 |
6 33
|
jca |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( `' F ` P ) e. A /\ -. ( `' F ` P ) .<_ W ) ) |