Theorem 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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cvsdiv.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cvsdivcl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cvsdiv.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		cvsdiv.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	cvsdiv	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) )
4		simpl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝑊 ∈ ℂVec )
5	4	cvslvec	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝑊 ∈ LVec )
6	1	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
7		drngring	⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
8	5 6 7	3syl	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐹 ∈ Ring )
9		simpr1	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ 𝐾 )
10		simpr2	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ 𝐾 )
11		simpr3	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
12		eldifsn	⊢ ( 𝐵 ∈ ( 𝐾 ∖ { 0 } ) ↔ ( 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) )
13	10 11 12	sylanbrc	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ( 𝐾 ∖ { 0 } ) )
14	1 2	cvsunit	⊢ ( 𝑊 ∈ ℂVec → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )
15	14	adantr	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )
16	13 15	eleqtrd	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ( Unit ‘ 𝐹 ) )
17		eqid	⊢ ( Unit ‘ 𝐹 ) = ( Unit ‘ 𝐹 )
18		eqid	⊢ ( /r ‘ 𝐹 ) = ( /r ‘ 𝐹 )
19	2 17 18	dvrcl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ ( Unit ‘ 𝐹 ) ) → ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) ∈ 𝐾 )
20	8 9 16 19	syl3anc	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) ∈ 𝐾 )
21	3 20	eqeltrd	⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )