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 ≤ 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )