Metamath Proof Explorer

Theorem osumcllem4N

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 osumcllem4N 
|- ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> q =/= r )

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 n0i 
 |-  ( r e. ( X i^i Y ) -> -. ( X i^i Y ) = (/) )
10 incom 
 |-  ( X i^i Y ) = ( Y i^i X )
11 sslin 
 |-  ( X C_ ( ._|_ ` Y ) -> ( Y i^i X ) C_ ( Y i^i ( ._|_ ` Y ) ) )
12 11 3ad2ant3 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( Y i^i X ) C_ ( Y i^i ( ._|_ ` Y ) ) )
13 10 12 eqsstrid 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( X i^i Y ) C_ ( Y i^i ( ._|_ ` Y ) ) )
14 3 5 pnonsingN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( Y i^i ( ._|_ ` Y ) ) = (/) )
15 14 3adant3 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( Y i^i ( ._|_ ` Y ) ) = (/) )
16 13 15 sseqtrd 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( X i^i Y ) C_ (/) )
17 ss0b 
 |-  ( ( X i^i Y ) C_ (/) <-> ( X i^i Y ) = (/) )
18 16 17 sylib 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( X i^i Y ) = (/) )
19 18 adantr 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> ( X i^i Y ) = (/) )
20 9 19 nsyl3 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> -. r e. ( X i^i Y ) )
21 simprr 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> q e. Y )
22 eleq1w 
 |-  ( q = r -> ( q e. Y <-> r e. Y ) )
23 21 22 syl5ibcom 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> ( q = r -> r e. Y ) )
24 simprl 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> r e. X )
25 23 24 jctild 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> ( q = r -> ( r e. X /\ r e. Y ) ) )
26 elin 
 |-  ( r e. ( X i^i Y ) <-> ( r e. X /\ r e. Y ) )
27 25 26 imbitrrdi 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> ( q = r -> r e. ( X i^i Y ) ) )
28 27 necon3bd 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> ( -. r e. ( X i^i Y ) -> q =/= r ) )
29 20 28 mpd 
 |-  ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> q =/= r )