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 | ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( +ℎ “ ( 𝐴 × 𝐵 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpeq12 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 × 𝑦 ) = ( 𝐴 × 𝐵 ) ) | |
| 2 | 1 | imaeq2d | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( +ℎ “ ( 𝑥 × 𝑦 ) ) = ( +ℎ “ ( 𝐴 × 𝐵 ) ) ) |
| 3 | df-shs | ⊢ +ℋ = ( 𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ ( 𝑥 × 𝑦 ) ) ) | |
| 4 | hilablo | ⊢ +ℎ ∈ AbelOp | |
| 5 | imaexg | ⊢ ( +ℎ ∈ AbelOp → ( +ℎ “ ( 𝐴 × 𝐵 ) ) ∈ V ) | |
| 6 | 4 5 | ax-mp | ⊢ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ∈ V |
| 7 | 2 3 6 | ovmpoa | ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( +ℎ “ ( 𝐴 × 𝐵 ) ) ) |