Theorem cphdivcl

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

	Ref	Expression
Hypotheses	cphsca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphsca.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cphdivcl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cphsca.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	cphsubrg	⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4	3	adantr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
5		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
6	5	subrgss	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
7	4 6	syl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐾 ⊆ ℂ )
8		simpr1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ 𝐾 )
9	7 8	sseldd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
10		simpr2	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ 𝐾 )
11	7 10	sseldd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
12		simpr3	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
13	9 11 12	divrecd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
14	1 2	cphreccl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ 𝐾 )
15	14	3adant3r1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 1 / 𝐵 ) ∈ 𝐾 )
16		cnfldmul	⊢ · = ( .r ‘ ℂfld )
17	16	subrgmcl	⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ ( 1 / 𝐵 ) ∈ 𝐾 ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ 𝐾 )
18	4 8 15 17	syl3anc	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ 𝐾 )
19	13 18	eqeltrd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )