This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Lemma for paddass . Combine paddasslem5 and paddasslem6 . (Contributed by NM, 9-Jan-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | paddasslem.l | |- .<_ = ( le ` K ) |
|
| paddasslem.j | |- .\/ = ( join ` K ) |
||
| paddasslem.a | |- A = ( Atoms ` K ) |
||
| Assertion | paddasslem7 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | paddasslem.l | |- .<_ = ( le ` K ) |
|
| 2 | paddasslem.j | |- .\/ = ( join ` K ) |
|
| 3 | paddasslem.a | |- A = ( Atoms ` K ) |
|
| 4 | simpl1 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> K e. HL ) |
|
| 5 | simpl21 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> p e. A ) |
|
| 6 | simpl23 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> s e. A ) |
|
| 7 | 5 6 | jca | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> ( p e. A /\ s e. A ) ) |
| 8 | simpl33 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> z e. A ) |
|
| 9 | simpl22 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> r e. A ) |
|
| 10 | simpl3 | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> ( x e. A /\ y e. A /\ z e. A ) ) |
|
| 11 | simprl | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) ) |
|
| 12 | 1 2 3 | paddasslem5 | |- ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) ) -> s =/= z ) |
| 13 | 4 9 10 11 12 | syl31anc | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> s =/= z ) |
| 14 | simprr | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> s .<_ ( p .\/ z ) ) |
|
| 15 | 1 2 3 | paddasslem6 | |- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) ) |
| 16 | 4 7 8 13 14 15 | syl32anc | |- ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ s e. A ) /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) ) |