cphsqrtcl2

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

	Ref	Expression
Hypotheses	cphsca.f	$⊢ F = Scalar (W)$
	cphsca.k	$⊢ K = {Base}_{F}$
Assertion	cphsqrtcl2	$⊢ (W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \to \sqrt{A} \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3		sqrt0	$⊢ \sqrt{0} = 0$
4		fveq2	$⊢ A = 0 \to \sqrt{A} = \sqrt{0}$
5		id	$⊢ A = 0 \to A = 0$
6	3 4 5	3eqtr4a	$⊢ A = 0 \to \sqrt{A} = A$
7	6	adantl	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A = 0) \to \sqrt{A} = A$
8		simpl2	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A = 0) \to A \in K$
9	7 8	eqeltrd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A = 0) \to \sqrt{A} \in K$
10		simpl1	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to W \in CPreHil$
11	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
12	10 11	syl	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to K \in SubRing (ℂ_{fld})$
13		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
14	13	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
15	12 14	syl	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to K \subseteq ℂ$
16		simpl2	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to A \in K$
17	1 2	cphabscl	$⊢ (W \in CPreHil \land A \in K) \to \|A\| \in K$
18	10 16 17	syl2anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| \in K$
19	15 16	sseldd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to A \in ℂ$
20	19	abscld	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| \in ℝ$
21	19	absge0d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to 0 \leq \|A\|$
22	1 2	cphsqrtcl	$⊢ (W \in CPreHil \land (\|A\| \in K \land \|A\| \in ℝ \land 0 \leq \|A\|)) \to \sqrt{\|A\|} \in K$
23	10 18 20 21 22	syl13anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \sqrt{\|A\|} \in K$
24		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
25	24	subrgacl	$⊢ (K \in SubRing (ℂ_{fld}) \land \|A\| \in K \land A \in K) \to \|A\| + A \in K$
26	12 18 16 25	syl3anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| + A \in K$
27	1 2	cphabscl	$⊢ (W \in CPreHil \land \|A\| + A \in K) \to \|\|A\| + A\| \in K$
28	10 26 27	syl2anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|\|A\| + A\| \in K$
29	15 26	sseldd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| + A \in ℂ$
30		simpl3	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \neg - A \in ℝ^{+}$
31	20	recnd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| \in ℂ$
32	31 19	subnegd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| - (- A) = \|A\| + A$
33	32	eqeq1d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\|A\| - (- A) = 0 \leftrightarrow \|A\| + A = 0)$
34	19	negcld	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to - A \in ℂ$
35	31 34	subeq0ad	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\|A\| - (- A) = 0 \leftrightarrow \|A\| = - A)$
36	33 35	bitr3d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\|A\| + A = 0 \leftrightarrow \|A\| = - A)$
37		absrpcl	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ^{+}$
38	19 37	sylancom	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| \in ℝ^{+}$
39		eleq1	$⊢ \|A\| = - A \to (\|A\| \in ℝ^{+} \leftrightarrow - A \in ℝ^{+})$
40	38 39	syl5ibcom	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\|A\| = - A \to - A \in ℝ^{+})$
41	36 40	sylbid	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\|A\| + A = 0 \to - A \in ℝ^{+})$
42	41	necon3bd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to (\neg - A \in ℝ^{+} \to \|A\| + A \neq 0)$
43	30 42	mpd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|A\| + A \neq 0$
44	29 43	absne0d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \|\|A\| + A\| \neq 0$
45	1 2	cphdivcl	$⊢ (W \in CPreHil \land (\|A\| + A \in K \land \|\|A\| + A\| \in K \land \|\|A\| + A\| \neq 0)) \to \frac{\|A\| + A}{\|\|A\| + A\|} \in K$
46	10 26 28 44 45	syl13anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \frac{\|A\| + A}{\|\|A\| + A\|} \in K$
47		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
48	47	subrgmcl	$⊢ (K \in SubRing (ℂ_{fld}) \land \sqrt{\|A\|} \in K \land \frac{\|A\| + A}{\|\|A\| + A\|} \in K) \to \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in K$
49	12 23 46 48	syl3anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in K$
50	15 49	sseldd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in ℂ$
51		eqid	$⊢ \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})$
52	51	sqreulem	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to ({\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A \land 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})) \land i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})$
53	19 43 52	syl2anc	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to ({\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A \land 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})) \land i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})$
54	53	simp1d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to {\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A$
55	53	simp2d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}))$
56	53	simp3d	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+}$
57		df-nel	$⊢ i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+} \leftrightarrow \neg i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in ℝ^{+}$
58	56 57	sylib	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \neg i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in ℝ^{+}$
59	50 19 54 55 58	eqsqrtd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) = \sqrt{A}$
60	59 49	eqeltrrd	$⊢ ((W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \land A \neq 0) \to \sqrt{A} \in K$
61	9 60	pm2.61dane	$⊢ (W \in CPreHil \land A \in K \land \neg - A \in ℝ^{+}) \to \sqrt{A} \in K$

Metamath Proof Explorer

Theorem cphsqrtcl2

Proof