Step |
Hyp |
Ref |
Expression |
1 |
|
islvol3.b |
|- B = ( Base ` K ) |
2 |
|
islvol3.l |
|- .<_ = ( le ` K ) |
3 |
|
islvol3.j |
|- .\/ = ( join ` K ) |
4 |
|
islvol3.a |
|- A = ( Atoms ` K ) |
5 |
|
islvol3.p |
|- P = ( LPlanes ` K ) |
6 |
|
islvol3.v |
|- V = ( LVols ` K ) |
7 |
|
eqid |
|- ( |
8 |
1 7 5 6
|
islvol4 |
|- ( ( K e. HL /\ X e. B ) -> ( X e. V <-> E. y e. P y ( |
9 |
|
simpll |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> K e. HL ) |
10 |
1 5
|
lplnbase |
|- ( y e. P -> y e. B ) |
11 |
10
|
adantl |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> y e. B ) |
12 |
|
simplr |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> X e. B ) |
13 |
1 2 3 7 4
|
cvrval3 |
|- ( ( K e. HL /\ y e. B /\ X e. B ) -> ( y ( E. p e. A ( -. p .<_ y /\ ( y .\/ p ) = X ) ) ) |
14 |
9 11 12 13
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> ( y ( E. p e. A ( -. p .<_ y /\ ( y .\/ p ) = X ) ) ) |
15 |
|
eqcom |
|- ( ( y .\/ p ) = X <-> X = ( y .\/ p ) ) |
16 |
15
|
a1i |
|- ( ( ( ( K e. HL /\ X e. B ) /\ y e. P ) /\ p e. A ) -> ( ( y .\/ p ) = X <-> X = ( y .\/ p ) ) ) |
17 |
16
|
anbi2d |
|- ( ( ( ( K e. HL /\ X e. B ) /\ y e. P ) /\ p e. A ) -> ( ( -. p .<_ y /\ ( y .\/ p ) = X ) <-> ( -. p .<_ y /\ X = ( y .\/ p ) ) ) ) |
18 |
17
|
rexbidva |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> ( E. p e. A ( -. p .<_ y /\ ( y .\/ p ) = X ) <-> E. p e. A ( -. p .<_ y /\ X = ( y .\/ p ) ) ) ) |
19 |
14 18
|
bitrd |
|- ( ( ( K e. HL /\ X e. B ) /\ y e. P ) -> ( y ( E. p e. A ( -. p .<_ y /\ X = ( y .\/ p ) ) ) ) |
20 |
19
|
rexbidva |
|- ( ( K e. HL /\ X e. B ) -> ( E. y e. P y ( E. y e. P E. p e. A ( -. p .<_ y /\ X = ( y .\/ p ) ) ) ) |
21 |
8 20
|
bitrd |
|- ( ( K e. HL /\ X e. B ) -> ( X e. V <-> E. y e. P E. p e. A ( -. p .<_ y /\ X = ( y .\/ p ) ) ) ) |