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

Metamath Proof Explorer

Theorem cphcjcl

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

Ref Expression
Hypotheses cphsca.f ⊢ F = Scalar ⁡ W
cphsca.k ⊢ K = Base F
Assertion cphcjcl ⊢ 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 cphsca ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K
4 3 fveq2d ⊢ W ∈ CPreHil → * F = * ℂ fld ↾ 𝑠 K
5 2 fvexi ⊢ K ∈ V
6 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
7 cnfldcj ⊢ * = * ℂ fld
8 6 7 ressstarv ⊢ K ∈ V → * = * ℂ fld ↾ 𝑠 K
9 5 8 ax-mp ⊢ * = * ℂ fld ↾ 𝑠 K
10 4 9 eqtr4di ⊢ W ∈ CPreHil → * F = *
11 10 adantr ⊢ W ∈ CPreHil ∧ A ∈ K → * F = *
12 11 fveq1d ⊢ W ∈ CPreHil ∧ A ∈ K → A * F = A ‾
13 cphphl ⊢ W ∈ CPreHil → W ∈ PreHil
14 1 phlsrng ⊢ W ∈ PreHil → F ∈ *-Ring
15 13 14 syl ⊢ W ∈ CPreHil → F ∈ *-Ring
16 eqid ⊢ * F = * F
17 16 2 srngcl ⊢ F ∈ *-Ring ∧ A ∈ K → A * F ∈ K
18 15 17 sylan ⊢ W ∈ CPreHil ∧ A ∈ K → A * F ∈ K
19 12 18 eqeltrrd ⊢ W ∈ CPreHil ∧ A ∈ K → A ‾ ∈ K