Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | shincl.1 | |- A e. SH |
|
shincl.2 | |- B e. SH |
||
shless.1 | |- C e. SH |
||
Assertion | shlej2i | |- ( A C_ B -> ( C vH A ) C_ ( C vH B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shincl.1 | |- A e. SH |
|
2 | shincl.2 | |- B e. SH |
|
3 | shless.1 | |- C e. SH |
|
4 | 1 2 3 | shlej1i | |- ( A C_ B -> ( A vH C ) C_ ( B vH C ) ) |
5 | 3 1 | shjcomi | |- ( C vH A ) = ( A vH C ) |
6 | 3 2 | shjcomi | |- ( C vH B ) = ( B vH C ) |
7 | 4 5 6 | 3sstr4g | |- ( A C_ B -> ( C vH A ) C_ ( C vH B ) ) |