Step |
Hyp |
Ref |
Expression |
1 |
|
pexmidlem.l |
|- .<_ = ( le ` K ) |
2 |
|
pexmidlem.j |
|- .\/ = ( join ` K ) |
3 |
|
pexmidlem.a |
|- A = ( Atoms ` K ) |
4 |
|
pexmidlem.p |
|- .+ = ( +P ` K ) |
5 |
|
pexmidlem.o |
|- ._|_ = ( _|_P ` K ) |
6 |
|
pexmidlem.m |
|- M = ( X .+ { p } ) |
7 |
|
n0 |
|- ( ( ( ._|_ ` X ) i^i M ) =/= (/) <-> E. q q e. ( ( ._|_ ` X ) i^i M ) ) |
8 |
1 2 3 4 5 6
|
pexmidlem4N |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) ) |
9 |
8
|
expr |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ X =/= (/) ) -> ( q e. ( ( ._|_ ` X ) i^i M ) -> p e. ( X .+ ( ._|_ ` X ) ) ) ) |
10 |
9
|
exlimdv |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ X =/= (/) ) -> ( E. q q e. ( ( ._|_ ` X ) i^i M ) -> p e. ( X .+ ( ._|_ ` X ) ) ) ) |
11 |
7 10
|
syl5bi |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ X =/= (/) ) -> ( ( ( ._|_ ` X ) i^i M ) =/= (/) -> p e. ( X .+ ( ._|_ ` X ) ) ) ) |
12 |
11
|
necon1bd |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ X =/= (/) ) -> ( -. p e. ( X .+ ( ._|_ ` X ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) ) ) |
13 |
12
|
impr |
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) ) |