Step |
Hyp |
Ref |
Expression |
1 |
|
lvolnelpln.p |
|- P = ( LPlanes ` K ) |
2 |
|
lvolnelpln.v |
|- V = ( LVols ` K ) |
3 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
4 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
5 |
4 2
|
lvolbase |
|- ( X e. V -> X e. ( Base ` K ) ) |
6 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
7 |
4 6
|
latref |
|- ( ( K e. Lat /\ X e. ( Base ` K ) ) -> X ( le ` K ) X ) |
8 |
3 5 7
|
syl2an |
|- ( ( K e. HL /\ X e. V ) -> X ( le ` K ) X ) |
9 |
6 1 2
|
lvolnlelpln |
|- ( ( K e. HL /\ X e. V /\ X e. P ) -> -. X ( le ` K ) X ) |
10 |
9
|
3expia |
|- ( ( K e. HL /\ X e. V ) -> ( X e. P -> -. X ( le ` K ) X ) ) |
11 |
8 10
|
mt2d |
|- ( ( K e. HL /\ X e. V ) -> -. X e. P ) |