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=BaseF
Assertion cvsdiv ⊢W∈ℂVec∧A∈K∧B∈K∧B≠0→AB=A/r⁡FB

Proof

Step Hyp Ref Expression
1 cvsdiv.f ⊢F=Scalar⁡W
2 cvsdiv.k ⊢K=BaseF
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→AB=A/r⁡ℂfld↾𝑠KB
24 6 7 18 23 syl3anc ⊢W∈ℂVec∧A∈K∧B∈K∧B≠0→AB=A/r⁡ℂfld↾𝑠KB
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⁡FB=A/r⁡ℂfld↾𝑠KB
27 24 26 eqtr4d ⊢W∈ℂVec∧A∈K∧B∈K∧B≠0→AB=A/r⁡FB