Step |
Hyp |
Ref |
Expression |
1 |
|
lplnri1.j |
|- .\/ = ( join ` K ) |
2 |
|
lplnri1.a |
|- A = ( Atoms ` K ) |
3 |
|
lplnri1.p |
|- P = ( LPlanes ` K ) |
4 |
|
lplnri1.y |
|- Y = ( ( Q .\/ R ) .\/ S ) |
5 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
6 |
5 1 2 3 4
|
islpln2ah |
|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( Y e. P <-> ( Q =/= R /\ -. S ( le ` K ) ( Q .\/ R ) ) ) ) |
7 |
6
|
biimp3a |
|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( Q =/= R /\ -. S ( le ` K ) ( Q .\/ R ) ) ) |
8 |
7
|
simpld |
|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> Q =/= R ) |