Theorem 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 {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shsidmi	$$⊢A{+}_{\mathscr{H}}A=A$$

Proof

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