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 ⊢ 𝐴 ∈ Sℋ
Assertion shsidmi ( 𝐴 +ℋ 𝐴 ) = 𝐴

Proof

Step Hyp Ref Expression
1 shsidm.1 ⊢ 𝐴 ∈ Sℋ
2 1 1 shseli ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +ℎ 𝑧 ) )
3 shaddcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 +ℎ 𝑧 ) ∈ 𝐴 )
4 1 3 mp3an1 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 +ℎ 𝑧 ) ∈ 𝐴 )
5 eleq1 ⊢ ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝑦 +ℎ 𝑧 ) ∈ 𝐴 ) )
6 4 5 syl5ibrcom ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 ) )
7 6 rexlimivv ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ 𝐴 )
8 2 7 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐴 ) → 𝑥 ∈ 𝐴 )
9 8 ssriv ⊢ ( 𝐴 +ℋ 𝐴 ) ⊆ 𝐴
10 1 1 shsub1i ⊢ 𝐴 ⊆ ( 𝐴 +ℋ 𝐴 )
11 9 10 eqssi ⊢ ( 𝐴 +ℋ 𝐴 ) = 𝐴