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 e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )

Proof

Step Hyp Ref Expression
1 cvsdiv.f 
 |-  F = ( Scalar ` W )
2 cvsdiv.k 
 |-  K = ( Base ` F )
3 1 2 cvsdiv 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) = ( A ( /r ` F ) B ) )
4 simpl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> W e. CVec )
5 4 cvslvec 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> W e. LVec )
6 1 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
7 drngring 
 |-  ( F e. DivRing -> F e. Ring )
8 5 6 7 3syl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> F e. Ring )
9 simpr1 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> A e. K )
10 simpr2 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. K )
11 simpr3 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B =/= 0 )
12 eldifsn 
 |-  ( B e. ( K \ { 0 } ) <-> ( B e. K /\ B =/= 0 ) )
13 10 11 12 sylanbrc 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. ( K \ { 0 } ) )
14 1 2 cvsunit 
 |-  ( W e. CVec -> ( K \ { 0 } ) = ( Unit ` F ) )
15 14 adantr 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( K \ { 0 } ) = ( Unit ` F ) )
16 13 15 eleqtrd 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. ( Unit ` F ) )
17 eqid 
 |-  ( Unit ` F ) = ( Unit ` F )
18 eqid 
 |-  ( /r ` F ) = ( /r ` F )
19 2 17 18 dvrcl 
 |-  ( ( F e. Ring /\ A e. K /\ B e. ( Unit ` F ) ) -> ( A ( /r ` F ) B ) e. K )
20 8 9 16 19 syl3anc 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A ( /r ` F ) B ) e. K )
21 3 20 eqeltrd 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )