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

Proof

Step Hyp Ref Expression
1 cphsca.f 
 |-  F = ( Scalar ` W )
2 cphsca.k 
 |-  K = ( Base ` F )
3 simpl1 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> W e. CPreHil )
4 1 2 cphsubrg 
 |-  ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
5 3 4 syl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> K e. ( SubRing ` CCfld ) )
6 cnfldbas 
 |-  CC = ( Base ` CCfld )
7 6 subrgss 
 |-  ( K e. ( SubRing ` CCfld ) -> K C_ CC )
8 5 7 syl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> K C_ CC )
9 simpl3 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> A e. K )
10 8 9 sseldd 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> A e. CC )
11 10 negnegd 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> -u -u A = A )
12 11 fveq2d 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( sqrt ` -u -u A ) = ( sqrt ` A ) )
13 rpre 
 |-  ( -u A e. RR+ -> -u A e. RR )
14 13 adantl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> -u A e. RR )
15 rpge0 
 |-  ( -u A e. RR+ -> 0 <_ -u A )
16 15 adantl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> 0 <_ -u A )
17 14 16 sqrtnegd 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( sqrt ` -u -u A ) = ( _i x. ( sqrt ` -u A ) ) )
18 12 17 eqtr3d 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( sqrt ` A ) = ( _i x. ( sqrt ` -u A ) ) )
19 simpl2 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> _i e. K )
20 cnfldneg 
 |-  ( A e. CC -> ( ( invg ` CCfld ) ` A ) = -u A )
21 10 20 syl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( ( invg ` CCfld ) ` A ) = -u A )
22 subrgsubg 
 |-  ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
23 5 22 syl 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> K e. ( SubGrp ` CCfld ) )
24 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
25 24 subginvcl 
 |-  ( ( K e. ( SubGrp ` CCfld ) /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) e. K )
26 23 9 25 syl2anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( ( invg ` CCfld ) ` A ) e. K )
27 21 26 eqeltrrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> -u A e. K )
28 1 2 cphsqrtcl 
 |-  ( ( W e. CPreHil /\ ( -u A e. K /\ -u A e. RR /\ 0 <_ -u A ) ) -> ( sqrt ` -u A ) e. K )
29 3 27 14 16 28 syl13anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( sqrt ` -u A ) e. K )
30 cnfldmul 
 |-  x. = ( .r ` CCfld )
31 30 subrgmcl 
 |-  ( ( K e. ( SubRing ` CCfld ) /\ _i e. K /\ ( sqrt ` -u A ) e. K ) -> ( _i x. ( sqrt ` -u A ) ) e. K )
32 5 19 29 31 syl3anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( _i x. ( sqrt ` -u A ) ) e. K )
33 18 32 eqeltrd 
 |-  ( ( ( W e. CPreHil /\ _i e. K /\ A e. K ) /\ -u A e. RR+ ) -> ( sqrt ` A ) e. K )
34 33 ex 
 |-  ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( -u A e. RR+ -> ( sqrt ` A ) e. K ) )
35 1 2 cphsqrtcl2 
 |-  ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqrt ` A ) e. K )
36 35 3expia 
 |-  ( ( W e. CPreHil /\ A e. K ) -> ( -. -u A e. RR+ -> ( sqrt ` A ) e. K ) )
37 36 3adant2 
 |-  ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( -. -u A e. RR+ -> ( sqrt ` A ) e. K ) )
38 34 37 pm2.61d 
 |-  ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( sqrt ` A ) e. K )