Theorem rrxvsca

Description: The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023)

	Ref	Expression
Hypotheses	rrxval.r
	rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
	rrxvsca.r	$$⊢\underset{\dot{}}{\bullet }={\cdot }_H$$
	rrxvsca.i	$$⊢\phi \to I\in V$$
	rrxvsca.j	$$⊢\phi \to J\in I$$
	rrxvsca.a	$$⊢\phi \to A\in ℝ$$
	rrxvsca.x	$$⊢\phi \to X\in {\mathrm{Base}}_H$$
Assertion	rrxvsca	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=AX\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
3		rrxvsca.r	$$⊢\underset{\dot{}}{\bullet }={\cdot }_H$$
4		rrxvsca.i	$$⊢\phi \to I\in V$$
5		rrxvsca.j	$$⊢\phi \to J\in I$$
6		rrxvsca.a	$$⊢\phi \to A\in ℝ$$
7		rrxvsca.x	$$⊢\phi \to X\in {\mathrm{Base}}_H$$
8	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
9	4 8	syl	$$⊢\phi \to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
10	9	fveq2d	$$⊢\phi \to {\cdot }_H={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
11	3 10	syl5eq	$$⊢\phi \to \underset{\dot{}}{\bullet }={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
12	11	oveqd	$$⊢\phi \to A\underset{\dot{}}{\bullet }X=A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X$$
13	12	fveq1d	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=\left(A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X\right)\left(J\right)$$
14		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
15		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
16		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
17	9	fveq2d	$$⊢\phi \to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
18		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
19	18 15	tcphbas	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
20	17 19	syl6eqr	$$⊢\phi \to {\mathrm{Base}}_H={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
21	7 20	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
22		eqid	$$⊢{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
23	18 22	tcphvsca	$$⊢{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
24	23	eqcomi	$$⊢{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
25		remulr	$$⊢\times ={\cdot }_{{ℝ}_{\mathrm{fld}}}$$
26	14 15 16 4 6 21 5 24 25	frlmvscaval	$$⊢\phi \to \left(A{\cdot }_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}X\right)\left(J\right)=AX\left(J\right)$$
27	13 26	eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)\left(J\right)=AX\left(J\right)$$