Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cphsqrcl3 Structured version   Unicode version

Theorem cphsqrcl3 19142
 Description: If the scalar field contains , it is completely closed under square roots (i.e. it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.)
Hypotheses
Ref Expression
cphsca.f Scalar
cphsca.k
Assertion
Ref Expression
cphsqrcl3

Proof of Theorem cphsqrcl3
StepHypRef Expression
1 simpl1 960 . . . . . . . . . 10
2 cphsca.f . . . . . . . . . . 11 Scalar
3 cphsca.k . . . . . . . . . . 11
42, 3cphsubrg 19135 . . . . . . . . . 10 SubRingfld
51, 4syl 16 . . . . . . . . 9 SubRingfld
6 cnfldbas 16699 . . . . . . . . . 10 fld
76subrgss 15861 . . . . . . . . 9 SubRingfld
85, 7syl 16 . . . . . . . 8
9 simpl3 962 . . . . . . . 8
108, 9sseldd 3341 . . . . . . 7
1110negnegd 9394 . . . . . 6
1211fveq2d 5724 . . . . 5
13 rpre 10610 . . . . . . 7
1413adantl 453 . . . . . 6
15 rpge0 10616 . . . . . . 7
1615adantl 453 . . . . . 6
1714, 16sqrnegd 12216 . . . . 5
1812, 17eqtr3d 2469 . . . 4
19 simpl2 961 . . . . 5
20 cnfldneg 16719 . . . . . . . 8 fld
2110, 20syl 16 . . . . . . 7 fld
22 subrgsubg 15866 . . . . . . . . 9 SubRingfld SubGrpfld
235, 22syl 16 . . . . . . . 8 SubGrpfld
24 eqid 2435 . . . . . . . . 9 fld fld
2524subginvcl 14945 . . . . . . . 8 SubGrpfld fld
2623, 9, 25syl2anc 643 . . . . . . 7 fld
2721, 26eqeltrrd 2510 . . . . . 6
282, 3cphsqrcl 19139 . . . . . 6
291, 27, 14, 16, 28syl13anc 1186 . . . . 5
30 cnfldmul 16701 . . . . . 6 fld
3130subrgmcl 15872 . . . . 5 SubRingfld
325, 19, 29, 31syl3anc 1184 . . . 4
3318, 32eqeltrd 2509 . . 3
3433ex 424 . 2
352, 3cphsqrcl2 19141 . . . 4
36353expia 1155 . . 3