Description: A 1-dimensional subspace is less than or equal to any member of CH containing its generating vector. (Contributed by NM, 30-May-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ch1dle | |- ( ( A e. CH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chsh | |- ( A e. CH -> A e. SH ) |
|
| 2 | sh1dle | |- ( ( A e. SH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A ) |
|
| 3 | 1 2 | sylan | |- ( ( A e. CH /\ B e. A ) -> ( _|_ ` ( _|_ ` { B } ) ) C_ A ) |