cphabscl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	cphsca.f	$⊢ F = Scalar (W)$
	cphsca.k	$⊢ K = {Base}_{F}$
Assertion	cphabscl	$⊢ (W \in CPreHil \land A \in K) \to \|A\| \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
4		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
5	4	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
6	3 5	syl	$⊢ W \in CPreHil \to K \subseteq ℂ$
7	6	sselda	$⊢ (W \in CPreHil \land A \in K) \to A \in ℂ$
8		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
9	7 8	syl	$⊢ (W \in CPreHil \land A \in K) \to \|A\| = \sqrt{A \overline{A}}$
10		simpl	$⊢ (W \in CPreHil \land A \in K) \to W \in CPreHil$
11	3	adantr	$⊢ (W \in CPreHil \land A \in K) \to K \in SubRing (ℂ_{fld})$
12		simpr	$⊢ (W \in CPreHil \land A \in K) \to A \in K$
13	1 2	cphcjcl	$⊢ (W \in CPreHil \land A \in K) \to \overline{A} \in K$
14		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
15	14	subrgmcl	$⊢ (K \in SubRing (ℂ_{fld}) \land A \in K \land \overline{A} \in K) \to A \overline{A} \in K$
16	11 12 13 15	syl3anc	$⊢ (W \in CPreHil \land A \in K) \to A \overline{A} \in K$
17	7	cjmulrcld	$⊢ (W \in CPreHil \land A \in K) \to A \overline{A} \in ℝ$
18	7	cjmulge0d	$⊢ (W \in CPreHil \land A \in K) \to 0 \leq A \overline{A}$
19	1 2	cphsqrtcl	$⊢ (W \in CPreHil \land (A \overline{A} \in K \land A \overline{A} \in ℝ \land 0 \leq A \overline{A})) \to \sqrt{A \overline{A}} \in K$
20	10 16 17 18 19	syl13anc	$⊢ (W \in CPreHil \land A \in K) \to \sqrt{A \overline{A}} \in K$
21	9 20	eqeltrd	$⊢ (W \in CPreHil \land A \in K) \to \|A\| \in K$

Metamath Proof Explorer

Theorem cphabscl

Proof