Description: The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014) (Proof shortened by AV, 19-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lshpne0.v | |- V = ( Base ` W ) |
|
| lshpne0.n | |- N = ( LSpan ` W ) |
||
| lshpne0.p | |- .(+) = ( LSSum ` W ) |
||
| lshpne0.h | |- H = ( LSHyp ` W ) |
||
| lshpne0.o | |- .0. = ( 0g ` W ) |
||
| lshpne0.w | |- ( ph -> W e. LMod ) |
||
| lshpne0.u | |- ( ph -> U e. H ) |
||
| lshpne0.x | |- ( ph -> X e. V ) |
||
| lshpne0.e | |- ( ph -> ( U .(+) ( N ` { X } ) ) = V ) |
||
| Assertion | lshpne0 | |- ( ph -> X =/= .0. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lshpne0.v | |- V = ( Base ` W ) |
|
| 2 | lshpne0.n | |- N = ( LSpan ` W ) |
|
| 3 | lshpne0.p | |- .(+) = ( LSSum ` W ) |
|
| 4 | lshpne0.h | |- H = ( LSHyp ` W ) |
|
| 5 | lshpne0.o | |- .0. = ( 0g ` W ) |
|
| 6 | lshpne0.w | |- ( ph -> W e. LMod ) |
|
| 7 | lshpne0.u | |- ( ph -> U e. H ) |
|
| 8 | lshpne0.x | |- ( ph -> X e. V ) |
|
| 9 | lshpne0.e | |- ( ph -> ( U .(+) ( N ` { X } ) ) = V ) |
|
| 10 | eqid | |- ( LSubSp ` W ) = ( LSubSp ` W ) |
|
| 11 | 10 4 6 7 | lshplss | |- ( ph -> U e. ( LSubSp ` W ) ) |
| 12 | 1 2 3 4 6 7 8 9 | lshpnel | |- ( ph -> -. X e. U ) |
| 13 | 5 10 6 11 12 | lssvneln0 | |- ( ph -> X =/= .0. ) |