This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )