Theorem cphsqrtcl

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

	Ref	Expression
Hypotheses	cphsca.f	|- F = ( Scalar ` W )
	cphsca.k	|- K = ( Base ` F )
Assertion	cphsqrtcl	|- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqrt ` A ) e. K )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	|- F = ( Scalar ` W )
2		cphsca.k	|- K = ( Base ` F )
3		sqrtf	|- sqrt : CC --> CC
4		ffn	|- ( sqrt : CC --> CC -> sqrt Fn CC )
5	3 4	ax-mp	|- sqrt Fn CC
6		inss2	|- ( K i^i ( 0 [,) +oo ) ) C_ ( 0 [,) +oo )
7		rge0ssre	|- ( 0 [,) +oo ) C_ RR
8		ax-resscn	|- RR C_ CC
9	7 8	sstri	|- ( 0 [,) +oo ) C_ CC
10	6 9	sstri	|- ( K i^i ( 0 [,) +oo ) ) C_ CC
11		simp1	|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. K )
12		elrege0	|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
13	12	biimpri	|- ( ( A e. RR /\ 0 <_ A ) -> A e. ( 0 [,) +oo ) )
14	13	3adant1	|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. ( 0 [,) +oo ) )
15	11 14	elind	|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. ( K i^i ( 0 [,) +oo ) ) )
16		fnfvima	|- ( ( sqrt Fn CC /\ ( K i^i ( 0 [,) +oo ) ) C_ CC /\ A e. ( K i^i ( 0 [,) +oo ) ) ) -> ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) )
17	5 10 15 16	mp3an12i	|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) )
18		eqid	|- ( Base ` W ) = ( Base ` W )
19		eqid	|- ( .i ` W ) = ( .i ` W )
20		eqid	|- ( norm ` W ) = ( norm ` W )
21	18 19 20 1 2	iscph	|- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ ( norm ` W ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) ) )
22	21	simp2bi	|- ( W e. CPreHil -> ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K )
23	22	sselda	|- ( ( W e. CPreHil /\ ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) ) -> ( sqrt ` A ) e. K )
24	17 23	sylan2	|- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqrt ` A ) e. K )