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 ∧ 𝐴 ∈ 𝐾 ) → ( ∗ ‘ 𝐴 ) ∈ 𝐾 )