Metamath Proof Explorer

Theorem isch2

Description: Closed subspace H of a Hilbert space. Definition of Beran p. 107. (Contributed by NM, 17-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion isch2 ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H

Proof

Step Hyp Ref Expression
1 isch ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ⇝v H ℕ ⊆ H
2 alcom ⊢ ∀ f ∀ x f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ∀ x ∀ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H
3 19.23v ⊢ ∀ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ∃ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H
4 vex ⊢ x ∈ V
5 4 elima2 ⊢ x ∈ ⇝v H ℕ ↔ ∃ f f ∈ H ℕ ∧ f ⇝v x
6 5 imbi1i ⊢ x ∈ ⇝v H ℕ → x ∈ H ↔ ∃ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H
7 3 6 bitr4i ⊢ ∀ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ x ∈ ⇝v H ℕ → x ∈ H
8 7 albii ⊢ ∀ x ∀ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ∀ x x ∈ ⇝v H ℕ → x ∈ H
9 df-ss ⊢ ⇝v H ℕ ⊆ H ↔ ∀ x x ∈ ⇝v H ℕ → x ∈ H
10 8 9 bitr4i ⊢ ∀ x ∀ f f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ⇝v H ℕ ⊆ H
11 2 10 bitri ⊢ ∀ f ∀ x f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ⇝v H ℕ ⊆ H
12 nnex ⊢ ℕ ∈ V
13 elmapg ⊢ H ∈ S ℋ ∧ ℕ ∈ V → f ∈ H ℕ ↔ f : ℕ ⟶ H
14 12 13 mpan2 ⊢ H ∈ S ℋ → f ∈ H ℕ ↔ f : ℕ ⟶ H
15 14 anbi1d ⊢ H ∈ S ℋ → f ∈ H ℕ ∧ f ⇝v x ↔ f : ℕ ⟶ H ∧ f ⇝v x
16 15 imbi1d ⊢ H ∈ S ℋ → f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
17 16 2albidv ⊢ H ∈ S ℋ → ∀ f ∀ x f ∈ H ℕ ∧ f ⇝v x → x ∈ H ↔ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
18 11 17 bitr3id ⊢ H ∈ S ℋ → ⇝v H ℕ ⊆ H ↔ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
19 18 pm5.32i ⊢ H ∈ S ℋ ∧ ⇝v H ℕ ⊆ H ↔ H ∈ S ℋ ∧ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H
20 1 19 bitri ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ∀ f ∀ x f : ℕ ⟶ H ∧ f ⇝v x → x ∈ H