Metamath Proof Explorer

Theorem cphdivcl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses cphsca.f 
|- F = ( Scalar ` W )
cphsca.k 
|- K = ( Base ` F )
Assertion cphdivcl 
|- ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )

Proof

Step Hyp Ref Expression
1 cphsca.f 
 |-  F = ( Scalar ` W )
2 cphsca.k 
 |-  K = ( Base ` F )
3 1 2 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
4 3 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> K e. ( SubRing ` CCfld ) )
5 cnfldbas 
 |-  CC = ( Base ` CCfld )
6 5 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
7 4 6 syl 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> K C_ CC )
8 simpr1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> A e. K )
9 7 8 sseldd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> A e. CC )
10 simpr2 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. K )
11 7 10 sseldd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B e. CC )
12 simpr3 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> B =/= 0 )
13 9 11 12 divrecd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
14 1 2 cphreccl 
 |-  ( ( W e. CPreHil /\ B e. K /\ B =/= 0 ) -> ( 1 / B ) e. K )
15 14 3adant3r1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( 1 / B ) e. K )
16 cnfldmul 
 |-  x. = ( .r ` CCfld )
17 16 subrgmcl 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ A e. K /\ ( 1 / B ) e. K ) -> ( A x. ( 1 / B ) ) e. K )
18 4 8 15 17 syl3anc 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A x. ( 1 / B ) ) e. K )
19 13 18 eqeltrd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )