Theorem pexmidlem2N

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	pexmidlem2N	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )

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		simpl1	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> K e. HL )
8	7	hllatd	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> K e. Lat )
9		simpl2	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> X C_ A )
10	3 5	polssatN	|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
11	7 9 10	syl2anc	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> ( ._|_ ` X ) C_ A )
12		simpr1	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> r e. X )
13		simpr2	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> q e. ( ._|_ ` X ) )
14		simpl3	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p e. A )
15		simpr3	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p .<_ ( r .\/ q ) )
16	1 2 3 4	elpaddri	|- ( ( ( K e. Lat /\ X C_ A /\ ( ._|_ ` X ) C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ ( p e. A /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
17	8 9 11 12 13 14 15 16	syl322anc	|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )