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 ⊢ F = Scalar ⁡ W
cvsdiv.k ⊢ K = Base F
Assertion cvsdivcl ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A B ∈ K

Proof

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