Metamath Proof Explorer


Theorem shsval

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 ) → ( 𝐴 + 𝐵 ) = ( + “ ( 𝐴 × 𝐵 ) ) )

Proof

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 ) → ( 𝐴 + 𝐵 ) = ( + “ ( 𝐴 × 𝐵 ) ) )