Metamath Proof Explorer

Theorem cvsdiv

Description: Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)

Ref Expression
Hypotheses cvsdiv.f ⊢ F = Scalar ⁡ W
cvsdiv.k ⊢ K = Base F
Assertion cvsdiv ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A B = A / r ⁡ F B

Proof

Step Hyp Ref Expression
1 cvsdiv.f ⊢ F = Scalar ⁡ W
2 cvsdiv.k ⊢ K = Base F
3 simpl ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → W ∈ ℂVec
4 3 cvsclm ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → W ∈ CMod
5 1 2 clmsubrg ⊢ W ∈ CMod → K ∈ SubRing ⁡ ℂ fld
6 4 5 syl ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → K ∈ SubRing ⁡ ℂ fld
7 simpr1 ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A ∈ K
8 simpr2 ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → B ∈ K
9 simpr3 ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → B ≠ 0
10 eldifsn ⊢ B ∈ K ∖ 0 ↔ B ∈ K ∧ B ≠ 0
11 8 9 10 sylanbrc ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → B ∈ K ∖ 0
12 1 2 cvsunit ⊢ W ∈ ℂVec → K ∖ 0 = Unit ⁡ F
13 3 12 syl ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → K ∖ 0 = Unit ⁡ F
14 1 2 clmsca ⊢ W ∈ CMod → F = ℂ fld ↾ 𝑠 K
15 4 14 syl ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → F = ℂ fld ↾ 𝑠 K
16 15 fveq2d ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → Unit ⁡ F = Unit ⁡ ℂ fld ↾ 𝑠 K
17 13 16 eqtrd ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → K ∖ 0 = Unit ⁡ ℂ fld ↾ 𝑠 K
18 11 17 eleqtrd ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → B ∈ Unit ⁡ ℂ fld ↾ 𝑠 K
19 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
20 cnflddiv ⊢ ÷ = / r ⁡ ℂ fld
21 eqid ⊢ Unit ⁡ ℂ fld ↾ 𝑠 K = Unit ⁡ ℂ fld ↾ 𝑠 K
22 eqid ⊢ / r ⁡ ℂ fld ↾ 𝑠 K = / r ⁡ ℂ fld ↾ 𝑠 K
23 19 20 21 22 subrgdv ⊢ K ∈ SubRing ⁡ ℂ fld ∧ A ∈ K ∧ B ∈ Unit ⁡ ℂ fld ↾ 𝑠 K → A B = A / r ⁡ ℂ fld ↾ 𝑠 K B
24 6 7 18 23 syl3anc ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A B = A / r ⁡ ℂ fld ↾ 𝑠 K B
25 15 fveq2d ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → / r ⁡ F = / r ⁡ ℂ fld ↾ 𝑠 K
26 25 oveqd ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A / r ⁡ F B = A / r ⁡ ℂ fld ↾ 𝑠 K B
27 24 26 eqtr4d ⊢ W ∈ ℂVec ∧ A ∈ K ∧ B ∈ K ∧ B ≠ 0 → A B = A / r ⁡ F B