Theorem tcphcphlem2

Description: Lemma for tcphcph : homogeneity. (Contributed by Mario Carneiro, 8-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)$$
	tcphcph.3	$$⊢\left(\phi \wedge \left(x\in K\wedge x\in ℝ\wedge 0\le x\right)\right)\to \sqrt{x}\in K$$
	tcphcph.4	$$⊢\left(\phi \wedge x\in V\right)\to 0\le x\underset{\dot{}}{,}x$$
	tcphcph.k	$$⊢K={\mathrm{Base}}_F$$
	tcphcph.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	tcphcphlem2.3	$$⊢\phi \to X\in K$$
	tcphcphlem2.4	$$⊢\phi \to Y\in V$$
Assertion	tcphcphlem2	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)}=\left|X\right|\sqrt{Y\underset{\dot{}}{,}Y}$$

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		tcphcph.3	$$⊢\left(\phi \wedge \left(x\in K\wedge x\in ℝ\wedge 0\le x\right)\right)\to \sqrt{x}\in K$$
8		tcphcph.4	$$⊢\left(\phi \wedge x\in V\right)\to 0\le x\underset{\dot{}}{,}x$$
9		tcphcph.k	$$⊢K={\mathrm{Base}}_F$$
10		tcphcph.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
11		tcphcphlem2.3	$$⊢\phi \to X\in K$$
12		tcphcphlem2.4	$$⊢\phi \to Y\in V$$
13	1 2 3 4 5	phclm	$$⊢\phi \to W\in \mathrm{CMod}$$
14	3 9	clmsscn	$$⊢W\in \mathrm{CMod}\to K\subseteq ℂ$$
15	13 14	syl	$$⊢\phi \to K\subseteq ℂ$$
16	15 11	sseldd	$$⊢\phi \to X\in ℂ$$
17	16	cjmulrcld	$$⊢\phi \to X\bar{X}\in ℝ$$
18	16	cjmulge0d	$$⊢\phi \to 0\le X\bar{X}$$
19	1 2 3 4 5 6	tcphcphlem3	$$⊢\left(\phi \wedge Y\in V\right)\to Y\underset{\dot{}}{,}Y\in ℝ$$
20	12 19	mpdan	$$⊢\phi \to Y\underset{\dot{}}{,}Y\in ℝ$$
21		oveq12	$$⊢\left(x=Y\wedge x=Y\right)\to x\underset{\dot{}}{,}x=Y\underset{\dot{}}{,}Y$$
22	21	anidms	$$⊢x=Y\to x\underset{\dot{}}{,}x=Y\underset{\dot{}}{,}Y$$
23	22	breq2d	$$⊢x=Y\to \left(0\le x\underset{\dot{}}{,}x\leftrightarrow 0\le Y\underset{\dot{}}{,}Y\right)$$
24	8	ralrimiva	$$⊢\phi \to \forall x\in V0\le x\underset{\dot{}}{,}x$$
25	23 24 12	rspcdva	$$⊢\phi \to 0\le Y\underset{\dot{}}{,}Y$$
26	17 18 20 25	sqrtmuld	$$⊢\phi \to \sqrt{X\bar{X}\left(Y\underset{\dot{}}{,}Y\right)}=\sqrt{X\bar{X}}\sqrt{Y\underset{\dot{}}{,}Y}$$
27		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
28	4 27	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
29	2 3 10 9	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\wedge Y\in V\right)\to X\underset{\dot{}}{·}Y\in V$$
30	28 11 12 29	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in V$$
31		eqid	$$⊢{\cdot }_F={\cdot }_F$$
32		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
33	3 6 2 9 10 31 32	ipassr	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(X\underset{\dot{}}{·}Y\in V\wedge Y\in V\wedge X\in K\right)\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)=\left(\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y\right){\cdot }_F{X}^{{\mathrm{*}}_F}$$
34	4 30 12 11 33	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)=\left(\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y\right){\cdot }_F{X}^{{\mathrm{*}}_F}$$
35	3	clmmul	$$⊢W\in \mathrm{CMod}\to \times ={\cdot }_F$$
36	13 35	syl	$$⊢\phi \to \times ={\cdot }_F$$
37	36	oveqd	$$⊢\phi \to X\left(Y\underset{\dot{}}{,}Y\right)=X{\cdot }_F\left(Y\underset{\dot{}}{,}Y\right)$$
38	3 6 2 9 10 31	ipass	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(X\in K\wedge Y\in V\wedge Y\in V\right)\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y=X{\cdot }_F\left(Y\underset{\dot{}}{,}Y\right)$$
39	4 11 12 12 38	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y=X{\cdot }_F\left(Y\underset{\dot{}}{,}Y\right)$$
40	37 39	eqtr4d	$$⊢\phi \to X\left(Y\underset{\dot{}}{,}Y\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y$$
41	3	clmcj	$$⊢W\in \mathrm{CMod}\to *={\mathrm{*}}_F$$
42	13 41	syl	$$⊢\phi \to *={\mathrm{*}}_F$$
43	42	fveq1d	$$⊢\phi \to \bar{X}=X^{{\mathrm{*}}_F}$$
44	36 40 43	oveq123d	$$⊢\phi \to X\left(Y\underset{\dot{}}{,}Y\right)\bar{X}=\left(\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}Y\right){\cdot }_F{X}^{{\mathrm{*}}_F}$$
45	20	recnd	$$⊢\phi \to Y\underset{\dot{}}{,}Y\in ℂ$$
46	16	cjcld	$$⊢\phi \to \bar{X}\in ℂ$$
47	16 45 46	mul32d	$$⊢\phi \to X\left(Y\underset{\dot{}}{,}Y\right)\bar{X}=X\bar{X}\left(Y\underset{\dot{}}{,}Y\right)$$
48	34 44 47	3eqtr2d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)=X\bar{X}\left(Y\underset{\dot{}}{,}Y\right)$$
49	48	fveq2d	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)}=\sqrt{X\bar{X}\left(Y\underset{\dot{}}{,}Y\right)}$$
50		absval	$$⊢X\in ℂ\to \left|X\right|=\sqrt{X\bar{X}}$$
51	16 50	syl	$$⊢\phi \to \left|X\right|=\sqrt{X\bar{X}}$$
52	51	oveq1d	$$⊢\phi \to \left|X\right|\sqrt{Y\underset{\dot{}}{,}Y}=\sqrt{X\bar{X}}\sqrt{Y\underset{\dot{}}{,}Y}$$
53	26 49 52	3eqtr4d	$$⊢\phi \to \sqrt{\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{,}\left(X\underset{\dot{}}{·}Y\right)}=\left|X\right|\sqrt{Y\underset{\dot{}}{,}Y}$$