Metamath Proof Explorer

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	$⊢ F = Scalar (W)$
		cphsca.k	$⊢ K = {Base}_{F}$
	Assertion	cphdivcl	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
4	3	adantr	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to K \in SubRing (ℂ_{fld})$
5		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
6	5	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
7	4 6	syl	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to K \subseteq ℂ$
8		simpr1	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to A \in K$
9	7 8	sseldd	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to A \in ℂ$
10		simpr2	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to B \in K$
11	7 10	sseldd	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to B \in ℂ$
12		simpr3	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to B \neq 0$
13	9 11 12	divrecd	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} = A (\frac{1}{B})$
14	1 2	cphreccl	$⊢ (W \in CPreHil \land B \in K \land B \neq 0) \to \frac{1}{B} \in K$
15	14	3adant3r1	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to \frac{1}{B} \in K$
16		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
17	16	subrgmcl	$⊢ (K \in SubRing (ℂ_{fld}) \land A \in K \land \frac{1}{B} \in K) \to A (\frac{1}{B}) \in K$
18	4 8 15 17	syl3anc	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to A (\frac{1}{B}) \in K$
19	13 18	eqeltrd	$⊢ (W \in CPreHil \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} \in K$