Theorem rrxip

Description: The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	rrxval.r
	rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
Assertion	rrxip	$$⊢I\in V\to \left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)={\cdot }_{𝑖}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
3	1 2	rrxprds	$$⊢I\in V\to H=\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
4	3	fveq2d	$$⊢I\in V\to {\cdot }_{𝑖}\left(H\right)={\cdot }_{𝑖}\left(\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)\right)$$
5		eqid	$$⊢\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)=\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
6		eqid	$$⊢{\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)={\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
7	5 6	tcphip	$$⊢{\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)={\cdot }_{𝑖}\left(\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)\right)$$
8	2	fvexi	$$⊢B\in \mathrm{V}$$
9		eqid	$$⊢\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B=\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B$$
10		eqid	$$⊢{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)={\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)$$
11	9 10	ressip	$$⊢B\in \mathrm{V}\to {\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)={\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
12	8 11	ax-mp	$$⊢{\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)={\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)$$
13		eqid	$$⊢{ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)={ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)$$
14		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
15	14	a1i	$$⊢I\in V\to {ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
16		snex	$$⊢\left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\in \mathrm{V}$$
17		xpexg	$$⊢\left(I\in V\wedge \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\in \mathrm{V}\right)\to I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\in \mathrm{V}$$
18	16 17	mpan2	$$⊢I\in V\to I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\in \mathrm{V}$$
19		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}$$
20		fvex	$$⊢\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\in \mathrm{V}$$
21	20	snnz	$$⊢\left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\ne \varnothing$$
22		dmxp	$$⊢\left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\ne \varnothing \to \mathrm{dom}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)=I$$
23	21 22	ax-mp	$$⊢\mathrm{dom}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)=I$$
24	23	a1i	$$⊢I\in V\to \mathrm{dom}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)=I$$
25	13 15 18 19 24 10	prdsip	$$⊢I\in V\to {\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)=\left(f\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)},g\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}\left(f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)\right)\right)$$
26	13 15 18 19 24	prdsbas	$$⊢I\in V\to {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}=\underset{x\in I}{⨉}{\mathrm{Base}}_{\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)}$$
27		eqidd	$$⊢x\in I\to \mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)$$
28		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
29	28	eqimssi	$$⊢ℝ\subseteq {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
30	29	a1i	$$⊢x\in I\to ℝ\subseteq {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
31	27 30	srabase	$$⊢x\in I\to {\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}={\mathrm{Base}}_{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)}$$
32	28	a1i	$$⊢x\in I\to ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
33	20	fvconst2	$$⊢x\in I\to \left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)=\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)$$
34	33	fveq2d	$$⊢x\in I\to {\mathrm{Base}}_{\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)}={\mathrm{Base}}_{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)}$$
35	31 32 34	3eqtr4rd	$$⊢x\in I\to {\mathrm{Base}}_{\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)}=ℝ$$
36	35	adantl	$$⊢\left(I\in V\wedge x\in I\right)\to {\mathrm{Base}}_{\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)}=ℝ$$
37	36	ixpeq2dva	$$⊢I\in V\to \underset{x\in I}{⨉}{\mathrm{Base}}_{\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)}=\underset{x\in I}{⨉}ℝ$$
38		reex	$$⊢ℝ\in \mathrm{V}$$
39		ixpconstg	$$⊢\left(I\in V\wedge ℝ\in \mathrm{V}\right)\to \underset{x\in I}{⨉}ℝ={ℝ}^I$$
40	38 39	mpan2	$$⊢I\in V\to \underset{x\in I}{⨉}ℝ={ℝ}^I$$
41	26 37 40	3eqtrd	$$⊢I\in V\to {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}={ℝ}^I$$
42		remulr	$$⊢\times ={\cdot }_{{ℝ}_{\mathrm{fld}}}$$
43	33 30	sraip	$$⊢x\in I\to {\cdot }_{{ℝ}_{\mathrm{fld}}}={\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)$$
44	42 43	syl5req	$$⊢x\in I\to {\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)=\times$$
45	44	oveqd	$$⊢x\in I\to f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)=f\left(x\right)g\left(x\right)$$
46	45	mpteq2ia	$$⊢\left(x\in I⟼f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)\right)=\left(x\in I⟼f\left(x\right)g\left(x\right)\right)$$
47	46	a1i	$$⊢I\in V\to \left(x\in I⟼f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)\right)=\left(x\in I⟼f\left(x\right)g\left(x\right)\right)$$
48	47	oveq2d	$$⊢I\in V\to \underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}\left(f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)\right)=\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)$$
49	41 41 48	mpoeq123dv	$$⊢I\in V\to \left(f\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)},g\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)}⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}\left(f\left(x\right){\cdot }_{𝑖}\left(\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\left(x\right)\right)g\left(x\right)\right)\right)=\left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)$$
50	25 49	eqtrd	$$⊢I\in V\to {\cdot }_{𝑖}\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right)=\left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)$$
51	12 50	eqtr3id	$$⊢I\in V\to {\cdot }_{𝑖}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)=\left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)$$
52	7 51	eqtr3id	$$⊢I\in V\to {\cdot }_{𝑖}\left(\mathrm{toCPreHil}\left(\left({ℝ}_{\mathrm{fld}}{⨉}_{𝑠}\left(I\times \left\{\mathrm{subringAlg}\left({ℝ}_{\mathrm{fld}}\right)\left(ℝ\right)\right\}\right)\right){\upharpoonright }_{𝑠}B\right)\right)=\left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)$$
53	4 52	eqtr2d	$$⊢I\in V\to \left(f\in \left({ℝ}^I\right),g\in \left({ℝ}^I\right)⟼\underset{x\in I}{{\sum }_{{ℝ}_{\mathrm{fld}}}}f\left(x\right)g\left(x\right)\right)={\cdot }_{𝑖}\left(H\right)$$