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 syl6ibr
 |-  ( ( ( 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 )