Metamath Proof Explorer

Theorem osumcllem7N

Description: Lemma for osumclN . (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 osumcllem7N 
|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> 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 ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> K e. HL )
10 9 hllatd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> K e. Lat )
11 simp12 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> X C_ A )
12 simp23 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> p e. A )
13 simp22 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> X =/= (/) )
14 inss2 
 |-  ( Y i^i M ) C_ M
15 14 sseli 
 |-  ( q e. ( Y i^i M ) -> q e. M )
16 15 3ad2ant3 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> q e. M )
17 16 7 eleqtrdi 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> q e. ( X .+ { p } ) )
18 1 2 3 4 elpaddatiN 
 |-  ( ( ( K e. Lat /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( X .+ { p } ) ) ) -> E. r e. X q .<_ ( r .\/ p ) )
19 10 11 12 13 17 18 syl32anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> E. r e. X q .<_ ( r .\/ p ) )
20 simp11 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> ( K e. HL /\ X C_ A /\ Y C_ A ) )
21 simp121 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> X C_ ( ._|_ ` Y ) )
22 simp123 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> p e. A )
23 simp2 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> r e. X )
24 inss1 
 |-  ( Y i^i M ) C_ Y
25 simp13 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> q e. ( Y i^i M ) )
26 24 25 sseldi 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> q e. Y )
27 simp3 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> q .<_ ( r .\/ p ) )
28 1 2 3 4 5 6 7 8 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 ) )
29 20 21 22 23 26 27 28 syl123anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) /\ r e. X /\ q .<_ ( r .\/ p ) ) -> p e. ( X .+ Y ) )
30 29 rexlimdv3a 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> ( E. r e. X q .<_ ( r .\/ p ) -> p e. ( X .+ Y ) ) )
31 19 30 mpd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> p e. ( X .+ Y ) )