This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphsqrtcl ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 sqrtf ⊢ √ : ℂ ⟶ ℂ
4 ffn ⊢ ( √ : ℂ ⟶ ℂ → √ Fn ℂ )
5 3 4 ax-mp ⊢ √ Fn ℂ
6 inss2 ⊢ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ⊆ ( 0 [,) +∞ )
7 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 7 8 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
10 6 9 sstri ⊢ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ⊆ ℂ
11 simp1 ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ 𝐾 )
12 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
13 12 biimpri ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
14 13 3adant1 ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
15 11 14 elind ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 𝐾 ∩ ( 0 [,) +∞ ) ) )
16 fnfvima ⊢ ( ( √ Fn ℂ ∧ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ⊆ ℂ ∧ 𝐴 ∈ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) → ( √ ‘ 𝐴 ) ∈ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) )
17 5 10 15 16 mp3an12i ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) )
18 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
19 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
20 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
21 18 19 20 1 2 iscph ⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ ( norm ‘ 𝑊 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ) )
22 21 simp2bi ⊢ ( 𝑊 ∈ ℂPreHil → ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 )
23 22 sselda ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( √ ‘ 𝐴 ) ∈ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )
24 17 23 sylan2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )