Description: Value of subspace sum of two Hilbert space subspaces. Definition of subspace sum in Kalmbach p. 65. (Contributed by NM, 16-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | shsval | |- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( +h " ( A X. B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpeq12 | |- ( ( x = A /\ y = B ) -> ( x X. y ) = ( A X. B ) ) |
|
| 2 | 1 | imaeq2d | |- ( ( x = A /\ y = B ) -> ( +h " ( x X. y ) ) = ( +h " ( A X. B ) ) ) |
| 3 | df-shs | |- +H = ( x e. SH , y e. SH |-> ( +h " ( x X. y ) ) ) |
|
| 4 | hilablo | |- +h e. AbelOp |
|
| 5 | imaexg | |- ( +h e. AbelOp -> ( +h " ( A X. B ) ) e. _V ) |
|
| 6 | 4 5 | ax-mp | |- ( +h " ( A X. B ) ) e. _V |
| 7 | 2 3 6 | ovmpoa | |- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( +h " ( A X. B ) ) ) |