Theorem issh

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	issh	⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2	1	elpw2	⊢ ( 𝐻 ∈ 𝒫 ℋ ↔ 𝐻 ⊆ ℋ )
3		3anass	⊢ ( ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ↔ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )
4	2 3	anbi12i	⊢ ( ( 𝐻 ∈ 𝒫 ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ↔ ( 𝐻 ⊆ ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) )
5		eleq2	⊢ ( ℎ = 𝐻 → ( 0ℎ ∈ ℎ ↔ 0ℎ ∈ 𝐻 ) )
6		id	⊢ ( ℎ = 𝐻 → ℎ = 𝐻 )
7	6	sqxpeqd	⊢ ( ℎ = 𝐻 → ( ℎ × ℎ ) = ( 𝐻 × 𝐻 ) )
8	7	imaeq2d	⊢ ( ℎ = 𝐻 → ( +ℎ “ ( ℎ × ℎ ) ) = ( +ℎ “ ( 𝐻 × 𝐻 ) ) )
9	8 6	sseq12d	⊢ ( ℎ = 𝐻 → ( ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ↔ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ) )
10		xpeq2	⊢ ( ℎ = 𝐻 → ( ℂ × ℎ ) = ( ℂ × 𝐻 ) )
11	10	imaeq2d	⊢ ( ℎ = 𝐻 → ( ·ℎ “ ( ℂ × ℎ ) ) = ( ·ℎ “ ( ℂ × 𝐻 ) ) )
12	11 6	sseq12d	⊢ ( ℎ = 𝐻 → ( ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ↔ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) )
13	5 9 12	3anbi123d	⊢ ( ℎ = 𝐻 → ( ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) ↔ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )
14		df-sh	⊢ Sℋ = { ℎ ∈ 𝒫 ℋ ∣ ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) }
15	13 14	elrab2	⊢ ( 𝐻 ∈ Sℋ ↔ ( 𝐻 ∈ 𝒫 ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )
16		anass	⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ↔ ( 𝐻 ⊆ ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) )
17	4 15 16	3bitr4i	⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )