| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lshplss.s |
|- S = ( LSubSp ` W ) |
| 2 |
|
lshplss.h |
|- H = ( LSHyp ` W ) |
| 3 |
|
lshplss.w |
|- ( ph -> W e. LMod ) |
| 4 |
|
lshplss.u |
|- ( ph -> U e. H ) |
| 5 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 6 |
|
eqid |
|- ( LSpan ` W ) = ( LSpan ` W ) |
| 7 |
5 6 1 2
|
islshp |
|- ( W e. LMod -> ( U e. H <-> ( U e. S /\ U =/= ( Base ` W ) /\ E. v e. ( Base ` W ) ( ( LSpan ` W ) ` ( U u. { v } ) ) = ( Base ` W ) ) ) ) |
| 8 |
3 7
|
syl |
|- ( ph -> ( U e. H <-> ( U e. S /\ U =/= ( Base ` W ) /\ E. v e. ( Base ` W ) ( ( LSpan ` W ) ` ( U u. { v } ) ) = ( Base ` W ) ) ) ) |
| 9 |
4 8
|
mpbid |
|- ( ph -> ( U e. S /\ U =/= ( Base ` W ) /\ E. v e. ( Base ` W ) ( ( LSpan ` W ) ` ( U u. { v } ) ) = ( Base ` W ) ) ) |
| 10 |
9
|
simp1d |
|- ( ph -> U e. S ) |