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	⊢ ( 𝐴 +ℋ 𝐴 ) = 𝐴