cvsdivcl

Description: The scalar field of a subcomplex vector space is closed under division. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Hypotheses	cvsdiv.f	$⊢ F = Scalar (W)$
	cvsdiv.k	$⊢ K = {Base}_{F}$
Assertion	cvsdivcl	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} \in K$

Proof

Step	Hyp	Ref	Expression
1		cvsdiv.f	$⊢ F = Scalar (W)$
2		cvsdiv.k	$⊢ K = {Base}_{F}$
3	1 2	cvsdiv	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} = A /_{r} (F) B$
4		simpl	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to W \in ℂVec$
5	4	cvslvec	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to W \in LVec$
6	1	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
7		drngring	$⊢ F \in DivRing \to F \in Ring$
8	5 6 7	3syl	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to F \in Ring$
9		simpr1	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to A \in K$
10		simpr2	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to B \in K$
11		simpr3	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to B \neq 0$
12		eldifsn	$⊢ B \in (K ∖ \{0\}) \leftrightarrow (B \in K \land B \neq 0)$
13	10 11 12	sylanbrc	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to B \in (K ∖ \{0\})$
14	1 2	cvsunit	$⊢ W \in ℂVec \to K ∖ \{0\} = Unit (F)$
15	14	adantr	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to K ∖ \{0\} = Unit (F)$
16	13 15	eleqtrd	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to B \in Unit (F)$
17		eqid	$⊢ Unit (F) = Unit (F)$
18		eqid	$⊢ /_{r} (F) = /_{r} (F)$
19	2 17 18	dvrcl	$⊢ (F \in Ring \land A \in K \land B \in Unit (F)) \to A /_{r} (F) B \in K$
20	8 9 16 19	syl3anc	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to A /_{r} (F) B \in K$
21	3 20	eqeltrd	$⊢ (W \in ℂVec \land (A \in K \land B \in K \land B \neq 0)) \to \frac{A}{B} \in K$

Metamath Proof Explorer

Theorem cvsdivcl

Proof