Metamath Proof Explorer

Theorem osumcllem8N

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 osumcllem8N 
|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ -. p e. ( X .+ Y ) ) -> ( Y i^i M ) = (/) )

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 n0 
 |-  ( ( Y i^i M ) =/= (/) <-> E. q q e. ( Y i^i M ) )
10 1 2 3 4 5 6 7 8 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 ) )
11 10 3expia 
 |-  ( ( ( 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 ) ) )
12 11 exlimdv 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) ) -> ( E. q q e. ( Y i^i M ) -> p e. ( X .+ Y ) ) )
13 9 12 syl5bi 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) ) -> ( ( Y i^i M ) =/= (/) -> p e. ( X .+ Y ) ) )
14 13 necon1bd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) ) -> ( -. p e. ( X .+ Y ) -> ( Y i^i M ) = (/) ) )
15 14 3impia 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ -. p e. ( X .+ Y ) ) -> ( Y i^i M ) = (/) )