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	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A +_{ℋ} B = +_{ℎ} [A \times B]$

Proof

Step	Hyp	Ref	Expression
1		xpeq12	$⊢ (x = A \land y = B) \to x \times y = A \times B$
2	1	imaeq2d	$⊢ (x = A \land y = B) \to +_{ℎ} [x \times y] = +_{ℎ} [A \times B]$
3		df-shs	$⊢ +_{ℋ} = (x \in S_{ℋ}, y \in S_{ℋ} ⟼ +_{ℎ} [x \times y])$
4		hilablo	$⊢ +_{ℎ} \in AbelOp$
5		imaexg	$⊢ +_{ℎ} \in AbelOp \to +_{ℎ} [A \times B] \in V$
6	4 5	ax-mp	$⊢ +_{ℎ} [A \times B] \in V$
7	2 3 6	ovmpoa	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A +_{ℋ} B = +_{ℎ} [A \times B]$

Metamath Proof Explorer

Theorem shsval

Proof