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 e. SH
Assertion	shsidmi	|- ( A +H A ) = A

Proof

Step	Hyp	Ref	Expression
1		shsidm.1	|- A e. SH
2	1 1	shseli	|- ( x e. ( A +H A ) <-> E. y e. A E. z e. A x = ( y +h z ) )
3		shaddcl	|- ( ( A e. SH /\ y e. A /\ z e. A ) -> ( y +h z ) e. A )
4	1 3	mp3an1	|- ( ( y e. A /\ z e. A ) -> ( y +h z ) e. A )
5		eleq1	|- ( x = ( y +h z ) -> ( x e. A <-> ( y +h z ) e. A ) )
6	4 5	syl5ibrcom	|- ( ( y e. A /\ z e. A ) -> ( x = ( y +h z ) -> x e. A ) )
7	6	rexlimivv	|- ( E. y e. A E. z e. A x = ( y +h z ) -> x e. A )
8	2 7	sylbi	|- ( x e. ( A +H A ) -> x e. A )
9	8	ssriv	|- ( A +H A ) C_ A
10	1 1	shsub1i	|- A C_ ( A +H A )
11	9 10	eqssi	|- ( A +H A ) = A