Theorem cphabscl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	cphsca.f	|- F = ( Scalar ` W )
	cphsca.k	|- K = ( Base ` F )
Assertion	cphabscl	|- ( ( W e. CPreHil /\ A e. K ) -> ( abs ` A ) e. K )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	|- F = ( Scalar ` W )
2		cphsca.k	|- K = ( Base ` F )
3	1 2	cphsubrg	|- ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
4		cnfldbas	|- CC = ( Base ` CCfld )
5	4	subrgss	|- ( K e. ( SubRing ` CCfld ) -> K C_ CC )
6	3 5	syl	|- ( W e. CPreHil -> K C_ CC )
7	6	sselda	|- ( ( W e. CPreHil /\ A e. K ) -> A e. CC )
8		absval	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
9	7 8	syl	|- ( ( W e. CPreHil /\ A e. K ) -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
10		simpl	|- ( ( W e. CPreHil /\ A e. K ) -> W e. CPreHil )
11	3	adantr	|- ( ( W e. CPreHil /\ A e. K ) -> K e. ( SubRing ` CCfld ) )
12		simpr	|- ( ( W e. CPreHil /\ A e. K ) -> A e. K )
13	1 2	cphcjcl	|- ( ( W e. CPreHil /\ A e. K ) -> ( * ` A ) e. K )
14		cnfldmul	|- x. = ( .r ` CCfld )
15	14	subrgmcl	|- ( ( K e. ( SubRing ` CCfld ) /\ A e. K /\ ( * ` A ) e. K ) -> ( A x. ( * ` A ) ) e. K )
16	11 12 13 15	syl3anc	|- ( ( W e. CPreHil /\ A e. K ) -> ( A x. ( * ` A ) ) e. K )
17	7	cjmulrcld	|- ( ( W e. CPreHil /\ A e. K ) -> ( A x. ( * ` A ) ) e. RR )
18	7	cjmulge0d	|- ( ( W e. CPreHil /\ A e. K ) -> 0 <_ ( A x. ( * ` A ) ) )
19	1 2	cphsqrtcl	|- ( ( W e. CPreHil /\ ( ( A x. ( * ` A ) ) e. K /\ ( A x. ( * ` A ) ) e. RR /\ 0 <_ ( A x. ( * ` A ) ) ) ) -> ( sqrt ` ( A x. ( * ` A ) ) ) e. K )
20	10 16 17 18 19	syl13anc	|- ( ( W e. CPreHil /\ A e. K ) -> ( sqrt ` ( A x. ( * ` A ) ) ) e. K )
21	9 20	eqeltrd	|- ( ( W e. CPreHil /\ A e. K ) -> ( abs ` A ) e. K )