Theorem hsn0elch

Description: The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hsn0elch	⊢ { 0ℎ } ∈ Cℋ

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		snssi	⊢ ( 0ℎ ∈ ℋ → { 0ℎ } ⊆ ℋ )
3	1 2	ax-mp	⊢ { 0ℎ } ⊆ ℋ
4	1	elexi	⊢ 0ℎ ∈ V
5	4	snid	⊢ 0ℎ ∈ { 0ℎ }
6	3 5	pm3.2i	⊢ ( { 0ℎ } ⊆ ℋ ∧ 0ℎ ∈ { 0ℎ } )
7		velsn	⊢ ( 𝑥 ∈ { 0ℎ } ↔ 𝑥 = 0ℎ )
8		velsn	⊢ ( 𝑦 ∈ { 0ℎ } ↔ 𝑦 = 0ℎ )
9		oveq12	⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) = ( 0ℎ +ℎ 0ℎ ) )
10	1	hvaddlidi	⊢ ( 0ℎ +ℎ 0ℎ ) = 0ℎ
11	9 10	eqtrdi	⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) = 0ℎ )
12		ovex	⊢ ( 𝑥 +ℎ 𝑦 ) ∈ V
13	12	elsn	⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ↔ ( 𝑥 +ℎ 𝑦 ) = 0ℎ )
14	11 13	sylibr	⊢ ( ( 𝑥 = 0ℎ ∧ 𝑦 = 0ℎ ) → ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } )
15	7 8 14	syl2anb	⊢ ( ( 𝑥 ∈ { 0ℎ } ∧ 𝑦 ∈ { 0ℎ } ) → ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } )
16	15	rgen2	⊢ ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ }
17		oveq2	⊢ ( 𝑦 = 0ℎ → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ 0ℎ ) )
18		hvmul0	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ·ℎ 0ℎ ) = 0ℎ )
19	17 18	sylan9eqr	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = 0ℎ ) → ( 𝑥 ·ℎ 𝑦 ) = 0ℎ )
20		ovex	⊢ ( 𝑥 ·ℎ 𝑦 ) ∈ V
21	20	elsn	⊢ ( ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } ↔ ( 𝑥 ·ℎ 𝑦 ) = 0ℎ )
22	19 21	sylibr	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 = 0ℎ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
23	8 22	sylan2b	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ { 0ℎ } ) → ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
24	23	rgen2	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ }
25	16 24	pm3.2i	⊢ ( ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } )
26		issh2	⊢ ( { 0ℎ } ∈ Sℋ ↔ ( ( { 0ℎ } ⊆ ℋ ∧ 0ℎ ∈ { 0ℎ } ) ∧ ( ∀ 𝑥 ∈ { 0ℎ } ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 +ℎ 𝑦 ) ∈ { 0ℎ } ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ { 0ℎ } ( 𝑥 ·ℎ 𝑦 ) ∈ { 0ℎ } ) ) )
27	6 25 26	mpbir2an	⊢ { 0ℎ } ∈ Sℋ
28	4	fconst2	⊢ ( 𝑓 : ℕ ⟶ { 0ℎ } ↔ 𝑓 = ( ℕ × { 0ℎ } ) )
29		hlim0	⊢ ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ
30		breq1	⊢ ( 𝑓 = ( ℕ × { 0ℎ } ) → ( 𝑓 ⇝𝑣 0ℎ ↔ ( ℕ × { 0ℎ } ) ⇝𝑣 0ℎ ) )
31	29 30	mpbiri	⊢ ( 𝑓 = ( ℕ × { 0ℎ } ) → 𝑓 ⇝𝑣 0ℎ )
32	28 31	sylbi	⊢ ( 𝑓 : ℕ ⟶ { 0ℎ } → 𝑓 ⇝𝑣 0ℎ )
33		hlimuni	⊢ ( ( 𝑓 ⇝𝑣 0ℎ ∧ 𝑓 ⇝𝑣 𝑥 ) → 0ℎ = 𝑥 )
34	33	eleq1d	⊢ ( ( 𝑓 ⇝𝑣 0ℎ ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 0ℎ ∈ { 0ℎ } ↔ 𝑥 ∈ { 0ℎ } ) )
35	32 34	sylan	⊢ ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 0ℎ ∈ { 0ℎ } ↔ 𝑥 ∈ { 0ℎ } ) )
36	5 35	mpbii	⊢ ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } )
37	36	gen2	⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } )
38		isch2	⊢ ( { 0ℎ } ∈ Cℋ ↔ ( { 0ℎ } ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ { 0ℎ } ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ { 0ℎ } ) ) )
39	27 37 38	mpbir2an	⊢ { 0ℎ } ∈ Cℋ