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 ≀ 𝐴 ) ) β†’ ( √ β€˜ 𝐴 ) ∈ 𝐾 )