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 ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ) β†’ ( √ β€˜ 𝐴 ) ∈ 𝐾 )