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