Step |
Hyp |
Ref |
Expression |
1 |
|
lhpoc.b |
|- B = ( Base ` K ) |
2 |
|
lhpoc.o |
|- ._|_ = ( oc ` K ) |
3 |
|
lhpoc.a |
|- A = ( Atoms ` K ) |
4 |
|
lhpoc.h |
|- H = ( LHyp ` K ) |
5 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
6 |
1 2
|
opoccl |
|- ( ( K e. OP /\ W e. B ) -> ( ._|_ ` W ) e. B ) |
7 |
5 6
|
sylan |
|- ( ( K e. HL /\ W e. B ) -> ( ._|_ ` W ) e. B ) |
8 |
1 2 3 4
|
lhpoc |
|- ( ( K e. HL /\ ( ._|_ ` W ) e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) ) |
9 |
7 8
|
syldan |
|- ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) ) |
10 |
1 2
|
opococ |
|- ( ( K e. OP /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W ) |
11 |
5 10
|
sylan |
|- ( ( K e. HL /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W ) |
12 |
11
|
eleq1d |
|- ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` ( ._|_ ` W ) ) e. A <-> W e. A ) ) |
13 |
9 12
|
bitr2d |
|- ( ( K e. HL /\ W e. B ) -> ( W e. A <-> ( ._|_ ` W ) e. H ) ) |