| 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 /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> K e. HL ) |
| 5 |
|
simpl2r |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s e. A ) |
| 6 |
|
simpl2l |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p e. A ) |
| 7 |
|
simpl3 |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> z e. A ) |
| 8 |
5 6 7
|
3jca |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> ( s e. A /\ p e. A /\ z e. A ) ) |
| 9 |
|
simprl |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s =/= z ) |
| 10 |
4 8 9
|
3jca |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> ( K e. HL /\ ( s e. A /\ p e. A /\ z e. A ) /\ s =/= z ) ) |
| 11 |
|
simprr |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s .<_ ( p .\/ z ) ) |
| 12 |
1 2 3
|
hlatexch2 |
|- ( ( K e. HL /\ ( s e. A /\ p e. A /\ z e. A ) /\ s =/= z ) -> ( s .<_ ( p .\/ z ) -> p .<_ ( s .\/ z ) ) ) |
| 13 |
10 11 12
|
sylc |
|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) ) |