Theorem tcphcphlem3

Description: Lemma for tcphcph : real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
	tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
	tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
	tcphcph.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	tcphcphlem3	$$⊢\left(\phi \wedge X\in V\right)\to X\underset{\dot{}}{,}X\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphcph.v	$$⊢V={\mathrm{Base}}_W$$
3		tcphcph.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		tcphcph.1	$$⊢\phi \to W\in \mathrm{PreHil}$$
5		tcphcph.2	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
6		tcphcph.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
7	1 2 3 4 5	phclm	$$⊢\phi \to W\in \mathrm{CMod}$$
8	7	adantr	$$⊢\left(\phi \wedge X\in V\right)\to W\in \mathrm{CMod}$$
9		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
10	3 9	clmsscn	$$⊢W\in \mathrm{CMod}\to {\mathrm{Base}}_F\subseteq ℂ$$
11	8 10	syl	$$⊢\left(\phi \wedge X\in V\right)\to {\mathrm{Base}}_F\subseteq ℂ$$
12	3 6 2 9	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\wedge X\in V\right)\to X\underset{\dot{}}{,}X\in {\mathrm{Base}}_F$$
13	12	3anidm23	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\right)\to X\underset{\dot{}}{,}X\in {\mathrm{Base}}_F$$
14	4 13	sylan	$$⊢\left(\phi \wedge X\in V\right)\to X\underset{\dot{}}{,}X\in {\mathrm{Base}}_F$$
15	11 14	sseldd	$$⊢\left(\phi \wedge X\in V\right)\to X\underset{\dot{}}{,}X\in ℂ$$
16	3	clmcj	$$⊢W\in \mathrm{CMod}\to *={\mathrm{*}}_F$$
17	8 16	syl	$$⊢\left(\phi \wedge X\in V\right)\to *={\mathrm{*}}_F$$
18	17	fveq1d	$$⊢\left(\phi \wedge X\in V\right)\to \overline{X\underset{\dot{}}{,}X}={\left(X\underset{\dot{}}{,}X\right)}^{{\mathrm{*}}_F}$$
19	4	adantr	$$⊢\left(\phi \wedge X\in V\right)\to W\in \mathrm{PreHil}$$
20		simpr	$$⊢\left(\phi \wedge X\in V\right)\to X\in V$$
21		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
22	3 6 2 21	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge X\in V\wedge X\in V\right)\to {\left(X\underset{\dot{}}{,}X\right)}^{{\mathrm{*}}_F}=X\underset{\dot{}}{,}X$$
23	19 20 20 22	syl3anc	$$⊢\left(\phi \wedge X\in V\right)\to {\left(X\underset{\dot{}}{,}X\right)}^{{\mathrm{*}}_F}=X\underset{\dot{}}{,}X$$
24	18 23	eqtrd	$$⊢\left(\phi \wedge X\in V\right)\to \overline{X\underset{\dot{}}{,}X}=X\underset{\dot{}}{,}X$$
25	15 24	cjrebd	$$⊢\left(\phi \wedge X\in V\right)\to X\underset{\dot{}}{,}X\in ℝ$$