Theorem cphassi

Description: Associative law for the first argument of an inner product with scalar _ i . (Contributed by AV, 17-Oct-2021)

	Ref	Expression
Hypotheses	cphassi.x	$$⊢X={\mathrm{Base}}_W$$
	cphassi.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	cphassi.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphassi.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cphassi.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphassi	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to \left(\mathrm{i}\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A=\mathrm{i}\left(B\underset{\dot{}}{,}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cphassi.x	$$⊢X={\mathrm{Base}}_W$$
2		cphassi.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		cphassi.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
4		cphassi.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		cphassi.k	$$⊢K={\mathrm{Base}}_F$$
6		simp1l	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to W\in \mathrm{CPreHil}$$
7		simp1r	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to \mathrm{i}\in K$$
8		simp3	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to B\in X$$
9		simp2	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to A\in X$$
10	3 1 4 5 2	cphass	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(\mathrm{i}\in K\wedge B\in X\wedge A\in X\right)\right)\to \left(\mathrm{i}\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A=\mathrm{i}\left(B\underset{\dot{}}{,}A\right)$$
11	6 7 8 9 10	syl13anc	$$⊢\left(\left(W\in \mathrm{CPreHil}\wedge \mathrm{i}\in K\right)\wedge A\in X\wedge B\in X\right)\to \left(\mathrm{i}\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A=\mathrm{i}\left(B\underset{\dot{}}{,}A\right)$$