shsidmi

Description: Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	shsidm.1	$⊢ A \in S_{ℋ}$
	Assertion	shsidmi	$⊢ A +_{ℋ} A = A$

Step	Hyp	Ref	Expression
1		shsidm.1	$⊢ A \in S_{ℋ}$
2	1 1	shseli	$⊢ x \in (A +_{ℋ} A) \leftrightarrow \exists y \in A \exists z \in A x = y +_{ℎ} z$
3		shaddcl	$⊢ (A \in S_{ℋ} \land y \in A \land z \in A) \to y +_{ℎ} z \in A$
4	1 3	mp3an1	$⊢ (y \in A \land z \in A) \to y +_{ℎ} z \in A$
5		eleq1	$⊢ x = y +_{ℎ} z \to (x \in A \leftrightarrow y +_{ℎ} z \in A)$
6	4 5	syl5ibrcom	$⊢ (y \in A \land z \in A) \to (x = y +_{ℎ} z \to x \in A)$
7	6	rexlimivv	$⊢ \exists y \in A \exists z \in A x = y +_{ℎ} z \to x \in A$
8	2 7	sylbi	$⊢ x \in (A +_{ℋ} A) \to x \in A$
9	8	ssriv	$⊢ A +_{ℋ} A \subseteq A$
10	1 1	shsub1i	$⊢ A \subseteq A +_{ℋ} A$
11	9 10	eqssi	$⊢ A +_{ℋ} A = A$

Metamath Proof Explorer