This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphdivcl ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 cphsubrg ⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4 3 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
5 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
6 5 subrgss ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
7 4 6 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐾 ⊆ ℂ )
8 simpr1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ 𝐾 )
9 7 8 sseldd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
10 simpr2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ 𝐾 )
11 7 10 sseldd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
12 simpr3 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
13 9 11 12 divrecd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
14 1 2 cphreccl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ 𝐾 )
15 14 3adant3r1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 1 / 𝐵 ) ∈ 𝐾 )
16 cnfldmul ⊢ · = ( .r ‘ ℂfld )
17 16 subrgmcl ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ ( 1 / 𝐵 ) ∈ 𝐾 ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ 𝐾 )
18 4 8 15 17 syl3anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ 𝐾 )
19 13 18 eqeltrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ 𝐾 )