This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) ∈ 𝐾 )