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 e. CVec /\ ( A e. K /\ B e. 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 e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> W e. CVec )
4 3 cvsclm 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> W e. CMod )
5 1 2 clmsubrg 
 |-  ( W e. CMod -> K e. ( SubRing ` CCfld ) )
6 4 5 syl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> K e. ( SubRing ` CCfld ) )
7 simpr1 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> A e. K )
8 simpr2 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. K )
9 simpr3 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B =/= 0 )
10 eldifsn 
 |-  ( B e. ( K \ { 0 } ) <-> ( B e. K /\ B =/= 0 ) )
11 8 9 10 sylanbrc 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. ( K \ { 0 } ) )
12 1 2 cvsunit 
 |-  ( W e. CVec -> ( K \ { 0 } ) = ( Unit ` F ) )
13 3 12 syl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( K \ { 0 } ) = ( Unit ` F ) )
14 1 2 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s K ) )
15 4 14 syl 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> F = ( CCfld |`s K ) )
16 15 fveq2d 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( Unit ` F ) = ( Unit ` ( CCfld |`s K ) ) )
17 13 16 eqtrd 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( K \ { 0 } ) = ( Unit ` ( CCfld |`s K ) ) )
18 11 17 eleqtrd 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. ( Unit ` ( CCfld |`s K ) ) )
19 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
20 cnflddiv 
 |-  / = ( /r ` CCfld )
21 eqid 
 |-  ( Unit ` ( CCfld |`s K ) ) = ( Unit ` ( CCfld |`s K ) )
22 eqid 
 |-  ( /r ` ( CCfld |`s K ) ) = ( /r ` ( CCfld |`s K ) )
23 19 20 21 22 subrgdv 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ A e. K /\ B e. ( Unit ` ( CCfld |`s K ) ) ) -> ( A / B ) = ( A ( /r ` ( CCfld |`s K ) ) B ) )
24 6 7 18 23 syl3anc 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) = ( A ( /r ` ( CCfld |`s K ) ) B ) )
25 15 fveq2d 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( /r ` F ) = ( /r ` ( CCfld |`s K ) ) )
26 25 oveqd 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A ( /r ` F ) B ) = ( A ( /r ` ( CCfld |`s K ) ) B ) )
27 24 26 eqtr4d 
 |-  ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) = ( A ( /r ` F ) B ) )