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 ⊢ F = Scalar ⁡ W
cphsca.k ⊢ K = Base F
Assertion cphabscl ⊢ W ∈ CPreHil ∧ A ∈ K → A ∈ K

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ F = Scalar ⁡ W
2 cphsca.k ⊢ K = Base F
3 1 2 cphsubrg ⊢ W ∈ CPreHil → K ∈ SubRing ⁡ ℂ fld
4 cnfldbas ⊢ ℂ = Base ℂ fld
5 4 subrgss ⊢ K ∈ SubRing ⁡ ℂ fld → K ⊆ ℂ
6 3 5 syl ⊢ W ∈ CPreHil → K ⊆ ℂ
7 6 sselda ⊢ W ∈ CPreHil ∧ A ∈ K → A ∈ ℂ
8 absval ⊢ A ∈ ℂ → A = A ⁢ A ‾
9 7 8 syl ⊢ W ∈ CPreHil ∧ A ∈ K → A = A ⁢ A ‾
10 simpl ⊢ W ∈ CPreHil ∧ A ∈ K → W ∈ CPreHil
11 3 adantr ⊢ W ∈ CPreHil ∧ A ∈ K → K ∈ SubRing ⁡ ℂ fld
12 simpr ⊢ W ∈ CPreHil ∧ A ∈ K → A ∈ K
13 1 2 cphcjcl ⊢ W ∈ CPreHil ∧ A ∈ K → A ‾ ∈ K
14 cnfldmul ⊢ × = ⋅ ℂ fld
15 14 subrgmcl ⊢ K ∈ SubRing ⁡ ℂ fld ∧ A ∈ K ∧ A ‾ ∈ K → A ⁢ A ‾ ∈ K
16 11 12 13 15 syl3anc ⊢ W ∈ CPreHil ∧ A ∈ K → A ⁢ A ‾ ∈ K
17 7 cjmulrcld ⊢ W ∈ CPreHil ∧ A ∈ K → A ⁢ A ‾ ∈ ℝ
18 7 cjmulge0d ⊢ W ∈ CPreHil ∧ A ∈ K → 0 ≤ A ⁢ A ‾
19 1 2 cphsqrtcl ⊢ W ∈ CPreHil ∧ A ⁢ A ‾ ∈ K ∧ A ⁢ A ‾ ∈ ℝ ∧ 0 ≤ A ⁢ A ‾ → A ⁢ A ‾ ∈ K
20 10 16 17 18 19 syl13anc ⊢ W ∈ CPreHil ∧ A ∈ K → A ⁢ A ‾ ∈ K
21 9 20 eqeltrd ⊢ W ∈ CPreHil ∧ A ∈ K → A ∈ K