Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | shlub.1 | |- A e. SH |
|
| shlub.2 | |- B e. SH |
||
| shlub.3 | |- C e. CH |
||
| Assertion | shlubi | |- ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | shlub.1 | |- A e. SH |
|
| 2 | shlub.2 | |- B e. SH |
|
| 3 | shlub.3 | |- C e. CH |
|
| 4 | shlub | |- ( ( A e. SH /\ B e. SH /\ C e. CH ) -> ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) ) |
|
| 5 | 1 2 3 4 | mp3an | |- ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C ) |