Metamath Proof Explorer

Theorem cphsqrtcl2

Description: The scalar field of a subcomplex pre-Hilbert space is closed under square roots of all numbers except possibly the negative reals. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphsqrtcl2 ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 sqrt0 ⊢ ( √ ‘ 0 ) = 0
4 fveq2 ⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) )
5 id ⊢ ( 𝐴 = 0 → 𝐴 = 0 )
6 3 4 5 3eqtr4a ⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = 𝐴 )
7 6 adantl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 = 0 ) → ( √ ‘ 𝐴 ) = 𝐴 )
8 simpl2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 = 0 ) → 𝐴 ∈ 𝐾 )
9 7 8 eqeltrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 = 0 ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )
10 simpl1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 𝑊 ∈ ℂPreHil )
11 1 2 cphsubrg ⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
12 10 11 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
13 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
14 13 subrgss ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
15 12 14 syl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 𝐾 ⊆ ℂ )
16 simpl2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝐾 )
17 1 2 cphabscl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) ∈ 𝐾 )
18 10 16 17 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ 𝐾 )
19 15 16 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
20 19 abscld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
21 19 absge0d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 0 ≤ ( abs ‘ 𝐴 ) )
22 1 2 cphsqrtcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( abs ‘ 𝐴 ) ∈ 𝐾 ∧ ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ 𝐾 )
23 10 18 20 21 22 syl13anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ 𝐾 )
24 cnfldadd ⊢ + = ( +g ‘ ℂfld )
25 24 subrgacl ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( abs ‘ 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ 𝐾 )
26 12 18 16 25 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ 𝐾 )
27 1 2 cphabscl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ 𝐾 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ 𝐾 )
28 10 26 27 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ 𝐾 )
29 15 26 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
30 simpl3 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ¬ - 𝐴 ∈ ℝ+ )
31 20 recnd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
32 31 19 subnegd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) − - 𝐴 ) = ( ( abs ‘ 𝐴 ) + 𝐴 ) )
33 32 eqeq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ) )
34 19 negcld ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → - 𝐴 ∈ ℂ )
35 31 34 subeq0ad ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
36 33 35 bitr3d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
37 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
38 19 37 sylancom ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
39 eleq1 ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( abs ‘ 𝐴 ) ∈ ℝ+ ↔ - 𝐴 ∈ ℝ+ ) )
40 38 39 syl5ibcom ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) = - 𝐴 → - 𝐴 ∈ ℝ+ ) )
41 36 40 sylbid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 → - 𝐴 ∈ ℝ+ ) )
42 41 necon3bd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ¬ - 𝐴 ∈ ℝ+ → ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) )
43 30 42 mpd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 )
44 29 43 absne0d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 )
45 1 2 cphdivcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ 𝐾 ∧ ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ 𝐾 ∧ ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 ) ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ∈ 𝐾 )
46 10 26 28 44 45 syl13anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ∈ 𝐾 )
47 cnfldmul ⊢ · = ( .r ‘ ℂfld )
48 47 subrgmcl ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ 𝐾 ∧ ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ∈ 𝐾 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ 𝐾 )
49 12 23 46 48 syl3anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ 𝐾 )
50 15 49 sseldd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ ℂ )
51 eqid ⊢ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) )
52 51 sqreulem ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
53 19 43 52 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
54 53 simp1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 )
55 53 simp2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) )
56 53 simp3d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ )
57 df-nel ⊢ ( ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ↔ ¬ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∈ ℝ+ )
58 56 57 sylib ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ¬ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∈ ℝ+ )
59 50 19 54 55 58 eqsqrtd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) = ( √ ‘ 𝐴 ) )
60 59 49 eqeltrrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) ∧ 𝐴 ≠ 0 ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )
61 9 60 pm2.61dane ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝐾 ∧ ¬ - 𝐴 ∈ ℝ+ ) → ( √ ‘ 𝐴 ) ∈ 𝐾 )