Theorem 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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphsca.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cphabscl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cphsca.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	cphsubrg	⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
5	4	subrgss	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
6	3 5	syl	⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ⊆ ℂ )
7	6	sselda	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ℂ )
8		absval	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
9	7 8	syl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
10		simpl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → 𝑊 ∈ ℂPreHil )
11	3	adantr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
12		simpr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
13	1 2	cphcjcl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( ∗ ‘ 𝐴 ) ∈ 𝐾 )
14		cnfldmul	⊢ · = ( .r ‘ ℂfld )
15	14	subrgmcl	⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ ( ∗ ‘ 𝐴 ) ∈ 𝐾 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ 𝐾 )
16	11 12 13 15	syl3anc	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ 𝐾 )
17	7	cjmulrcld	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
18	7	cjmulge0d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
19	1 2	cphsqrtcl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ) → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ 𝐾 )
20	10 16 17 18 19	syl13anc	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ 𝐾 )
21	9 20	eqeltrd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) ∈ 𝐾 )