Metamath Proof Explorer

Theorem cphsqrtcl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under square roots of nonnegative reals. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsca.f ⊢ F = Scalar ⁡ W
cphsca.k ⊢ K = Base F
Assertion cphsqrtcl ⊢ W ∈ CPreHil ∧ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ K

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ F = Scalar ⁡ W
2 cphsca.k ⊢ K = Base F
3 sqrtf ⊢ √ : ℂ ⟶ ℂ
4 ffn ⊢ √ : ℂ ⟶ ℂ → √ Fn ℂ
5 3 4 ax-mp ⊢ √ Fn ℂ
6 inss2 ⊢ K ∩ 0 +∞ ⊆ 0 +∞
7 rge0ssre ⊢ 0 +∞ ⊆ ℝ
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 7 8 sstri ⊢ 0 +∞ ⊆ ℂ
10 6 9 sstri ⊢ K ∩ 0 +∞ ⊆ ℂ
11 simp1 ⊢ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ K
12 elrege0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A
13 12 biimpri ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ 0 +∞
14 13 3adant1 ⊢ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ 0 +∞
15 11 14 elind ⊢ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ K ∩ 0 +∞
16 fnfvima ⊢ √ Fn ℂ ∧ K ∩ 0 +∞ ⊆ ℂ ∧ A ∈ K ∩ 0 +∞ → A ∈ √ K ∩ 0 +∞
17 5 10 15 16 mp3an12i ⊢ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ √ K ∩ 0 +∞
18 eqid ⊢ Base W = Base W
19 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
20 eqid ⊢ norm ⁡ W = norm ⁡ W
21 18 19 20 1 2 iscph ⊢ W ∈ CPreHil ↔ W ∈ PreHil ∧ W ∈ NrmMod ∧ F = ℂ fld ↾ 𝑠 K ∧ √ K ∩ 0 +∞ ⊆ K ∧ norm ⁡ W = x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x
22 21 simp2bi ⊢ W ∈ CPreHil → √ K ∩ 0 +∞ ⊆ K
23 22 sselda ⊢ W ∈ CPreHil ∧ A ∈ √ K ∩ 0 +∞ → A ∈ K
24 17 23 sylan2 ⊢ W ∈ CPreHil ∧ A ∈ K ∧ A ∈ ℝ ∧ 0 ≤ A → A ∈ K