Theorem pexmidlem5N

Description: Lemma for pexmidN . (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidlem.l	|- .<_ = ( le ` K )
	pexmidlem.j	|- .\/ = ( join ` K )
	pexmidlem.a	|- A = ( Atoms ` K )
	pexmidlem.p	|- .+ = ( +P ` K )
	pexmidlem.o	|- ._|_ = ( _|_P ` K )
	pexmidlem.m	|- M = ( X .+ { p } )
Assertion	pexmidlem5N	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) )

Proof

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 ) = (/) )