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 \in CPreHil \land (A \in K \land A \in ℝ \land 0 \leq A)) \to \sqrt{A} \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
4		ffn	$⊢ \sqrt : ℂ ⟶ ℂ \to \sqrt Fn ℂ$
5	3 4	ax-mp	$⊢ \sqrt Fn ℂ$
6		inss2	$⊢ K \cap [0, +∞) \subseteq [0, +∞)$
7		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	7 8	sstri	$⊢ [0, +∞) \subseteq ℂ$
10	6 9	sstri	$⊢ K \cap [0, +∞) \subseteq ℂ$
11		simp1	$⊢ (A \in K \land A \in ℝ \land 0 \leq A) \to A \in K$
12		elrege0	$⊢ A \in [0, +∞) \leftrightarrow (A \in ℝ \land 0 \leq A)$
13	12	biimpri	$⊢ (A \in ℝ \land 0 \leq A) \to A \in [0, +∞)$
14	13	3adant1	$⊢ (A \in K \land A \in ℝ \land 0 \leq A) \to A \in [0, +∞)$
15	11 14	elind	$⊢ (A \in K \land A \in ℝ \land 0 \leq A) \to A \in (K \cap [0, +∞))$
16		fnfvima	$⊢ (\sqrt Fn ℂ \land K \cap [0, +∞) \subseteq ℂ \land A \in (K \cap [0, +∞))) \to \sqrt{A} \in \sqrt [K \cap [0, +∞)]$
17	5 10 15 16	mp3an12i	$⊢ (A \in K \land A \in ℝ \land 0 \leq A) \to \sqrt{A} \in \sqrt [K \cap [0, +∞)]$
18		eqid	$⊢ {Base}_{W} = {Base}_{W}$
19		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
20		eqid	$⊢ norm (W) = norm (W)$
21	18 19 20 1 2	iscph	$⊢ W \in CPreHil \leftrightarrow ((W \in PreHil \land W \in NrmMod \land F = ℂ_{fld} ↾_{𝑠} K) \land \sqrt [K \cap [0, +∞)] \subseteq K \land norm (W) = (x \in {Base}_{W} ⟼ \sqrt{x \cdot_{𝑖} (W) x}))$
22	21	simp2bi	$⊢ W \in CPreHil \to \sqrt [K \cap [0, +∞)] \subseteq K$
23	22	sselda	$⊢ (W \in CPreHil \land \sqrt{A} \in \sqrt [K \cap [0, +∞)]) \to \sqrt{A} \in K$
24	17 23	sylan2	$⊢ (W \in CPreHil \land (A \in K \land A \in ℝ \land 0 \leq A)) \to \sqrt{A} \in K$

Metamath Proof Explorer

Theorem cphsqrtcl

Proof