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

Metamath Proof Explorer

Theorem cphsqrtcl3

Description: If the scalar field of a subcomplex pre-Hilbert space contains the imaginary unit _i , then it is closed under square roots (i.e., it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphsqrtcl3 ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 simpl1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝑊 ∈ ℂPreHil )
4 1 2 cphsubrg ⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
5 3 4 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
6 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
7 6 subrgss ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
8 5 7 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝐾 ⊆ ℂ )
9 simpl3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 ∈ 𝐾 )
10 8 9 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
11 10 negnegd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → - - 𝐴 = 𝐴 )
12 11 fveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( √ ‘ - - 𝐴 ) = ( √ ‘ 𝐴 ) )
13 rpre ⊢ ( - 𝐴 ∈ ℝ+ → - 𝐴 ∈ ℝ )
14 13 adantl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → - 𝐴 ∈ ℝ )
15 rpge0 ⊢ ( - 𝐴 ∈ ℝ+ → 0 ≤ - 𝐴 )
16 15 adantl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 0 ≤ - 𝐴 )
17 14 16 sqrtnegd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( √ ‘ - - 𝐴 ) = ( i · ( √ ‘ - 𝐴 ) ) )
18 12 17 eqtr3d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( √ ‘ 𝐴 ) = ( i · ( √ ‘ - 𝐴 ) ) )
19 simpl2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → i ∈ 𝐾 )
20 cnfldneg ⊢ ( 𝐴 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
21 10 20 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
22 subrgsubg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
23 5 22 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
24 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
25 24 subginvcl ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) ∈ 𝐾 )
26 23 9 25 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) ∈ 𝐾 )
27 21 26 eqeltrrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → - 𝐴 ∈ 𝐾 )
28 1 2 cphsqrtcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( - 𝐴 ∈ 𝐾 ∧ - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) ) → ( √ ‘ - 𝐴 ) ∈ 𝐾 )
29 3 27 14 16 28 syl13anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( √ ‘ - 𝐴 ) ∈ 𝐾 )
30 cnfldmul ⊢ · = ( .r ‘ ℂfld )
31 30 subrgmcl ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ i ∈ 𝐾 ∧ ( √ ‘ - 𝐴 ) ∈ 𝐾 ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ 𝐾 )
32 5 19 29 31 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ 𝐾 )
33 18 32 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) ∧ - 𝐴 ∈ ℝ+ ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )
34 33 ex ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) → ( - 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ 𝐾 ) )
35 1 2 cphsqrtcl2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )
36 35 3expia ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( ¬ - 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ 𝐾 ) )
37 36 3adant2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) → ( ¬ - 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ 𝐾 ) )
38 34 37 pm2.61d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )