chlimi

Description: The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	chlim.1	⊢ 𝐴 ∈ V
	Assertion	chlimi	⊢ ( ( 𝐻 ∈ C_ℋ ∧ 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		chlim.1	⊢ 𝐴 ∈ V
2		isch2	⊢ ( 𝐻 ∈ C_ℋ ↔ ( 𝐻 ∈ S_ℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
3	2	simprbi	⊢ ( 𝐻 ∈ C_ℋ → ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
4		nnex	⊢ ℕ ∈ V
5		fex	⊢ ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ ℕ ∈ V ) → 𝐹 ∈ V )
6	4 5	mpan2	⊢ ( 𝐹 : ℕ ⟶ 𝐻 → 𝐹 ∈ V )
7	6	adantr	⊢ ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐹 ∈ V )
8		feq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ℕ ⟶ 𝐻 ↔ 𝐹 : ℕ ⟶ 𝐻 ) )
9		breq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ⇝_𝑣 𝑥 ↔ 𝐹 ⇝_𝑣 𝑥 ) )
10	8 9	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) ↔ ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) ) )
11	10	imbi1d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
12	11	albidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑥 ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
13	12	spcgv	⊢ ( 𝐹 ∈ V → ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ∀ 𝑥 ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
14		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ⇝_𝑣 𝑥 ↔ 𝐹 ⇝_𝑣 𝐴 ) )
15	14	anbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) ↔ ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) ) )
16		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐻 ↔ 𝐴 ∈ 𝐻 ) )
17	15 16	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) ) )
18	1 17	spcv	⊢ ( ∀ 𝑥 ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) )
19	13 18	syl6	⊢ ( 𝐹 ∈ V → ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) ) )
20	7 19	syl	⊢ ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) ) )
21	20	pm2.43b	⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝_𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) )
22	3 21	syl	⊢ ( 𝐻 ∈ C_ℋ → ( ( 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 ) )
23	22	3impib	⊢ ( ( 𝐻 ∈ C_ℋ ∧ 𝐹 : ℕ ⟶ 𝐻 ∧ 𝐹 ⇝_𝑣 𝐴 ) → 𝐴 ∈ 𝐻 )

Metamath Proof Explorer

Theorem chlimi

Proof