Metamath Proof Explorer

Theorem pexmidlem3N

Description: Lemma for pexmidN . Use atom exchange hlatexch1 to swap p and q . (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 pexmidlem3N 
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> 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 simp1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> ( K e. HL /\ X C_ A /\ p e. A ) )
8 simp2l 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> r e. X )
9 simp2r 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> q e. ( ._|_ ` X ) )
10 simpl1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> K e. HL )
11 simpl2 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> X C_ A )
12 3 5 polssatN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
13 10 11 12 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( ._|_ ` X ) C_ A )
14 simprr 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q e. ( ._|_ ` X ) )
15 13 14 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q e. A )
16 simpl3 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> p e. A )
17 simprl 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> r e. X )
18 11 17 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> r e. A )
19 1 2 3 4 5 6 pexmidlem1N 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q =/= r )
20 19 3adantl3 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q =/= r )
21 1 2 3 hlatexch1 
 |-  ( ( K e. HL /\ ( q e. A /\ p e. A /\ r e. A ) /\ q =/= r ) -> ( q .<_ ( r .\/ p ) -> p .<_ ( r .\/ q ) ) )
22 10 15 16 18 20 21 syl131anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> ( q .<_ ( r .\/ p ) -> p .<_ ( r .\/ q ) ) )
23 22 3impia 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> p .<_ ( r .\/ q ) )
24 1 2 3 4 5 6 pexmidlem2N 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
25 7 8 9 23 24 syl13anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )