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 
|- F = ( Scalar ` W )
cphsca.k 
|- K = ( Base ` F )
Assertion cphsqrtcl2 
|- ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqrt ` A ) e. K )

Proof

Step Hyp Ref Expression
1 cphsca.f 
 |-  F = ( Scalar ` W )
2 cphsca.k 
 |-  K = ( Base ` F )
3 sqrt0 
 |-  ( sqrt ` 0 ) = 0
4 fveq2 
 |-  ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
5 id 
 |-  ( A = 0 -> A = 0 )
6 3 4 5 3eqtr4a 
 |-  ( A = 0 -> ( sqrt ` A ) = A )
7 6 adantl 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A = 0 ) -> ( sqrt ` A ) = A )
8 simpl2 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A = 0 ) -> A e. K )
9 7 8 eqeltrd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A = 0 ) -> ( sqrt ` A ) e. K )
10 simpl1 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> W e. CPreHil )
11 1 2 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
12 10 11 syl 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> K e. ( SubRing ` CCfld ) )
13 cnfldbas 
 |-  CC = ( Base ` CCfld )
14 13 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
15 12 14 syl 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> K C_ CC )
16 simpl2 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> A e. K )
17 1 2 cphabscl 
 |-  ( ( W e. CPreHil /\ A e. K ) -> ( abs ` A ) e. K )
18 10 16 17 syl2anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` A ) e. K )
19 15 16 sseldd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> A e. CC )
20 19 abscld 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` A ) e. RR )
21 19 absge0d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> 0 <_ ( abs ` A ) )
22 1 2 cphsqrtcl 
 |-  ( ( W e. CPreHil /\ ( ( abs ` A ) e. K /\ ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) -> ( sqrt ` ( abs ` A ) ) e. K )
23 10 18 20 21 22 syl13anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( sqrt ` ( abs ` A ) ) e. K )
24 cnfldadd 
 |-  + = ( +g ` CCfld )
25 24 subrgacl 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ ( abs ` A ) e. K /\ A e. K ) -> ( ( abs ` A ) + A ) e. K )
26 12 18 16 25 syl3anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( abs ` A ) + A ) e. K )
27 1 2 cphabscl 
 |-  ( ( W e. CPreHil /\ ( ( abs ` A ) + A ) e. K ) -> ( abs ` ( ( abs ` A ) + A ) ) e. K )
28 10 26 27 syl2anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` ( ( abs ` A ) + A ) ) e. K )
29 15 26 sseldd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( abs ` A ) + A ) e. CC )
30 simpl3 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> -. -u A e. RR+ )
31 20 recnd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` A ) e. CC )
32 31 19 subnegd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( abs ` A ) - -u A ) = ( ( abs ` A ) + A ) )
33 32 eqeq1d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) - -u A ) = 0 <-> ( ( abs ` A ) + A ) = 0 ) )
34 19 negcld 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> -u A e. CC )
35 31 34 subeq0ad 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) - -u A ) = 0 <-> ( abs ` A ) = -u A ) )
36 33 35 bitr3d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) + A ) = 0 <-> ( abs ` A ) = -u A ) )
37 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
38 19 37 sylancom 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
39 eleq1 
 |-  ( ( abs ` A ) = -u A -> ( ( abs ` A ) e. RR+ <-> -u A e. RR+ ) )
40 38 39 syl5ibcom 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( abs ` A ) = -u A -> -u A e. RR+ ) )
41 36 40 sylbid 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) + A ) = 0 -> -u A e. RR+ ) )
42 41 necon3bd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( -. -u A e. RR+ -> ( ( abs ` A ) + A ) =/= 0 ) )
43 30 42 mpd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( abs ` A ) + A ) =/= 0 )
44 29 43 absne0d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( abs ` ( ( abs ` A ) + A ) ) =/= 0 )
45 1 2 cphdivcl 
 |-  ( ( W e. CPreHil /\ ( ( ( abs ` A ) + A ) e. K /\ ( abs ` ( ( abs ` A ) + A ) ) e. K /\ ( abs ` ( ( abs ` A ) + A ) ) =/= 0 ) ) -> ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) e. K )
46 10 26 28 44 45 syl13anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) e. K )
47 cnfldmul 
 |-  x. = ( .r ` CCfld )
48 47 subrgmcl 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ ( sqrt ` ( abs ` A ) ) e. K /\ ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) e. K ) -> ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) e. K )
49 12 23 46 48 syl3anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) e. K )
50 15 49 sseldd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) e. CC )
51 eqid 
 |-  ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) = ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) )
52 51 sqreulem 
 |-  ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) /\ ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) )
53 19 43 52 syl2anc 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A /\ 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) /\ ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ ) )
54 53 simp1d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ^ 2 ) = A )
55 53 simp2d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> 0 <_ ( Re ` ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) )
56 53 simp3d 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ )
57 df-nel 
 |-  ( ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e/ RR+ <-> -. ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e. RR+ )
58 56 57 sylib 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> -. ( _i x. ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) ) e. RR+ )
59 50 19 54 55 58 eqsqrtd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( ( sqrt ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) = ( sqrt ` A ) )
60 59 49 eqeltrrd 
 |-  ( ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) /\ A =/= 0 ) -> ( sqrt ` A ) e. K )
61 9 60 pm2.61dane 
 |-  ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqrt ` A ) e. K )