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 CPreHil A K B K B 0 A B K

Proof

Step Hyp Ref Expression
1 cphsca.f F = Scalar W
2 cphsca.k K = Base F
3 1 2 cphsubrg W CPreHil K SubRing fld
4 3 adantr W CPreHil A K B K B 0 K SubRing fld
5 cnfldbas = Base fld
6 5 subrgss K SubRing fld K
7 4 6 syl W CPreHil A K B K B 0 K
8 simpr1 W CPreHil A K B K B 0 A K
9 7 8 sseldd W CPreHil A K B K B 0 A
10 simpr2 W CPreHil A K B K B 0 B K
11 7 10 sseldd W CPreHil A K B K B 0 B
12 simpr3 W CPreHil A K B K B 0 B 0
13 9 11 12 divrecd W CPreHil A K B K B 0 A B = A 1 B
14 1 2 cphreccl W CPreHil B K B 0 1 B K
15 14 3adant3r1 W CPreHil A K B K B 0 1 B K
16 cnfldmul × = fld
17 16 subrgmcl K SubRing fld A K 1 B K A 1 B K
18 4 8 15 17 syl3anc W CPreHil A K B K B 0 A 1 B K
19 13 18 eqeltrd W CPreHil A K B K B 0 A B K