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

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 cphsca ⊢ ( 𝑊 ∈ ℂPreHil → 𝐹 = ( ℂfld ↾s 𝐾 ) )
4 3 fveq2d ⊢ ( 𝑊 ∈ ℂPreHil → ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) ) )
5 2 fvexi ⊢ 𝐾 ∈ V
6 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
7 cnfldcj ⊢ ∗ = ( *𝑟 ‘ ℂfld )
8 6 7 ressstarv ⊢ ( 𝐾 ∈ V → ∗ = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) ) )
9 5 8 ax-mp ⊢ ∗ = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) )
10 4 9 eqtr4di ⊢ ( 𝑊 ∈ ℂPreHil → ( *𝑟 ‘ 𝐹 ) = ∗ )
11 10 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( *𝑟 ‘ 𝐹 ) = ∗ )
12 11 fveq1d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) = ( ∗ ‘ 𝐴 ) )
13 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
14 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
15 13 14 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝐹 ∈ *-Ring )
16 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
17 16 2 srngcl ⊢ ( ( 𝐹 ∈ *-Ring ∧ 𝐴 ∈ 𝐾 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
18 15 17 sylan ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
19 12 18 eqeltrrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( ∗ ‘ 𝐴 ) ∈ 𝐾 )