Metamath Proof Explorer


Theorem shsss

Description: The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion shsss ASBSA+B

Proof

Step Hyp Ref Expression
1 shsval ASBSA+B=+A×B
2 imassrn +A×Bran+
3 ax-hfvadd +:×
4 frn +:×ran+
5 3 4 ax-mp ran+
6 2 5 sstri +A×B
7 1 6 eqsstrdi ASBSA+B