Theorem cnmpt1ip

Description: Continuity of inner product; analogue of cnmpt12f which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cnmpt1ip.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	cnmpt1ip.c	$$⊢C=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	cnmpt1ip.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cnmpt1ip.r	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	cnmpt1ip.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(X\right)$$
	cnmpt1ip.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(K\mathrm{Cn}J\right)$$
	cnmpt1ip.b	$$⊢\phi \to \left(x\in X⟼B\right)\in \left(K\mathrm{Cn}J\right)$$
Assertion	cnmpt1ip	$$⊢\phi \to \left(x\in X⟼A\underset{\dot{}}{,}B\right)\in \left(K\mathrm{Cn}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmpt1ip.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
2		cnmpt1ip.c	$$⊢C=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3		cnmpt1ip.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
4		cnmpt1ip.r	$$⊢\phi \to W\in \mathrm{CPreHil}$$
5		cnmpt1ip.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(X\right)$$
6		cnmpt1ip.a	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(K\mathrm{Cn}J\right)$$
7		cnmpt1ip.b	$$⊢\phi \to \left(x\in X⟼B\right)\in \left(K\mathrm{Cn}J\right)$$
8		cphngp	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{NrmGrp}$$
9		ngptps	$$⊢W\in \mathrm{NrmGrp}\to W\in \mathrm{TopSp}$$
10	4 8 9	3syl	$$⊢\phi \to W\in \mathrm{TopSp}$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12	11 1	istps	$$⊢W\in \mathrm{TopSp}\leftrightarrow J\in \mathrm{TopOn}\left({\mathrm{Base}}_W\right)$$
13	10 12	sylib	$$⊢\phi \to J\in \mathrm{TopOn}\left({\mathrm{Base}}_W\right)$$
14		cnf2	$$⊢\left(K\in \mathrm{TopOn}\left(X\right)\wedge J\in \mathrm{TopOn}\left({\mathrm{Base}}_W\right)\wedge \left(x\in X⟼A\right)\in \left(K\mathrm{Cn}J\right)\right)\to \left(x\in X⟼A\right):X⟶{\mathrm{Base}}_W$$
15	5 13 6 14	syl3anc	$$⊢\phi \to \left(x\in X⟼A\right):X⟶{\mathrm{Base}}_W$$
16	15	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to A\in {\mathrm{Base}}_W$$
17		cnf2	$$⊢\left(K\in \mathrm{TopOn}\left(X\right)\wedge J\in \mathrm{TopOn}\left({\mathrm{Base}}_W\right)\wedge \left(x\in X⟼B\right)\in \left(K\mathrm{Cn}J\right)\right)\to \left(x\in X⟼B\right):X⟶{\mathrm{Base}}_W$$
18	5 13 7 17	syl3anc	$$⊢\phi \to \left(x\in X⟼B\right):X⟶{\mathrm{Base}}_W$$
19	18	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to B\in {\mathrm{Base}}_W$$
20		eqid	$$⊢{\cdot }_{\mathrm{if}}\left(W\right)={\cdot }_{\mathrm{if}}\left(W\right)$$
21	11 3 20	ipfval	$$⊢\left(A\in {\mathrm{Base}}_W\wedge B\in {\mathrm{Base}}_W\right)\to A{\cdot }_{\mathrm{if}}\left(W\right)B=A\underset{\dot{}}{,}B$$
22	16 19 21	syl2anc	$$⊢\left(\phi \wedge x\in X\right)\to A{\cdot }_{\mathrm{if}}\left(W\right)B=A\underset{\dot{}}{,}B$$
23	22	mpteq2dva	$$⊢\phi \to \left(x\in X⟼A{\cdot }_{\mathrm{if}}\left(W\right)B\right)=\left(x\in X⟼A\underset{\dot{}}{,}B\right)$$
24	20 1 2	ipcn	$$⊢W\in \mathrm{CPreHil}\to {\cdot }_{\mathrm{if}}\left(W\right)\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}C\right)$$
25	4 24	syl	$$⊢\phi \to {\cdot }_{\mathrm{if}}\left(W\right)\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}C\right)$$
26	5 6 7 25	cnmpt12f	$$⊢\phi \to \left(x\in X⟼A{\cdot }_{\mathrm{if}}\left(W\right)B\right)\in \left(K\mathrm{Cn}C\right)$$
27	23 26	eqeltrrd	$$⊢\phi \to \left(x\in X⟼A\underset{\dot{}}{,}B\right)\in \left(K\mathrm{Cn}C\right)$$