This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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