Metamath Proof Explorer

Theorem osumcllem6N

Description: Lemma for osumclN . Use atom exchange hlatexch1 to swap p and q . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l 
|- .<_ = ( le ` K )
osumcllem.j 
|- .\/ = ( join ` K )
osumcllem.a 
|- A = ( Atoms ` K )
osumcllem.p 
|- .+ = ( +P ` K )
osumcllem.o 
|- ._|_ = ( _|_P ` K )
osumcllem.c 
|- C = ( PSubCl ` K )
osumcllem.m 
|- M = ( X .+ { p } )
osumcllem.u 
|- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
Assertion osumcllem6N 
|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> p e. ( X .+ Y ) )

Proof

Step Hyp Ref Expression
1 osumcllem.l 
 |-  .<_ = ( le ` K )
2 osumcllem.j 
 |-  .\/ = ( join ` K )
3 osumcllem.a 
 |-  A = ( Atoms ` K )
4 osumcllem.p 
 |-  .+ = ( +P ` K )
5 osumcllem.o 
 |-  ._|_ = ( _|_P ` K )
6 osumcllem.c 
 |-  C = ( PSubCl ` K )
7 osumcllem.m 
 |-  M = ( X .+ { p } )
8 osumcllem.u 
 |-  U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
9 simp11 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> K e. HL )
10 simp12 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> X C_ A )
11 simp13 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> Y C_ A )
12 simp2r 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> p e. A )
13 simp31 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> r e. X )
14 simp32 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> q e. Y )
15 11 14 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> q e. A )
16 10 13 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> r e. A )
17 15 12 16 3jca 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> ( q e. A /\ p e. A /\ r e. A ) )
18 simp2l 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> X C_ ( ._|_ ` Y ) )
19 1 2 3 4 5 6 7 8 osumcllem4N 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> q =/= r )
20 9 11 18 13 14 19 syl32anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> q =/= r )
21 9 17 20 3jca 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> ( K e. HL /\ ( q e. A /\ p e. A /\ r e. A ) /\ q =/= r ) )
22 simp33 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> q .<_ ( r .\/ p ) )
23 1 2 3 hlatexch1 
 |-  ( ( K e. HL /\ ( q e. A /\ p e. A /\ r e. A ) /\ q =/= r ) -> ( q .<_ ( r .\/ p ) -> p .<_ ( r .\/ q ) ) )
24 21 22 23 sylc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> p .<_ ( r .\/ q ) )
25 1 2 3 4 5 6 7 8 osumcllem5N 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ Y ) )
26 9 10 11 12 13 14 24 25 syl313anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> p e. ( X .+ Y ) )