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 \in CPreHil \land i \in K \land A \in K) \to \sqrt{A} \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3		simpl1	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to W \in CPreHil$
4	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
5	3 4	syl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to K \in SubRing (ℂ_{fld})$
6		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
7	6	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
8	5 7	syl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to K \subseteq ℂ$
9		simpl3	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to A \in K$
10	8 9	sseldd	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to A \in ℂ$
11	10	negnegd	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to - (- A) = A$
12	11	fveq2d	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to \sqrt{- (- A)} = \sqrt{A}$
13		rpre	$⊢ - A \in ℝ^{+} \to - A \in ℝ$
14	13	adantl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to - A \in ℝ$
15		rpge0	$⊢ - A \in ℝ^{+} \to 0 \leq - A$
16	15	adantl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to 0 \leq - A$
17	14 16	sqrtnegd	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to \sqrt{- (- A)} = i \sqrt{- A}$
18	12 17	eqtr3d	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to \sqrt{A} = i \sqrt{- A}$
19		simpl2	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to i \in K$
20		cnfldneg	$⊢ A \in ℂ \to {inv}_{g} (ℂ_{fld}) (A) = - A$
21	10 20	syl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to {inv}_{g} (ℂ_{fld}) (A) = - A$
22		subrgsubg	$⊢ K \in SubRing (ℂ_{fld}) \to K \in SubGrp (ℂ_{fld})$
23	5 22	syl	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to K \in SubGrp (ℂ_{fld})$
24		eqid	$⊢ {inv}_{g} (ℂ_{fld}) = {inv}_{g} (ℂ_{fld})$
25	24	subginvcl	$⊢ (K \in SubGrp (ℂ_{fld}) \land A \in K) \to {inv}_{g} (ℂ_{fld}) (A) \in K$
26	23 9 25	syl2anc	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to {inv}_{g} (ℂ_{fld}) (A) \in K$
27	21 26	eqeltrrd	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to - A \in K$
28	1 2	cphsqrtcl	$⊢ (W \in CPreHil \land (- A \in K \land - A \in ℝ \land 0 \leq - A)) \to \sqrt{- A} \in K$
29	3 27 14 16 28	syl13anc	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to \sqrt{- A} \in K$
30		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
31	30	subrgmcl	$⊢ (K \in SubRing (ℂ_{fld}) \land i \in K \land \sqrt{- A} \in K) \to i \sqrt{- A} \in K$
32	5 19 29 31	syl3anc	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to i \sqrt{- A} \in K$
33	18 32	eqeltrd	$⊢ ((W \in CPreHil \land i \in K \land A \in K) \land - A \in ℝ^{+}) \to \sqrt{A} \in K$
34	33	ex	$⊢ (W \in CPreHil \land i \in K \land A \in K) \to (- A \in ℝ^{+} \to \sqrt{A} \in K)$
35	1 2	cphsqrtcl2	$⊢ (W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \to \sqrt{A} \in K$
36	35	3expia	$⊢ (W \in CPreHil \land A \in K) \to (\neg - A \in ℝ^{+} \to \sqrt{A} \in K)$
37	36	3adant2	$⊢ (W \in CPreHil \land i \in K \land A \in K) \to (\neg - A \in ℝ^{+} \to \sqrt{A} \in K)$
38	34 37	pm2.61d	$⊢ (W \in CPreHil \land i \in K \land A \in K) \to \sqrt{A} \in K$

Metamath Proof Explorer

Theorem cphsqrtcl3

Proof