Theorem ipassr

Description: "Associative" law for second argument of inner product (compare ipass ). (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ipdir.f	$$⊢K={\mathrm{Base}}_F$$
	ipass.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	ipass.p	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
	ipassr.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_F$$
Assertion	ipassr	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{·}B\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ipdir.f	$$⊢K={\mathrm{Base}}_F$$
5		ipass.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		ipass.p	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
7		ipassr.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_F$$
8		simpl	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to W\in \mathrm{PreHil}$$
9		simpr3	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to C\in K$$
10		simpr2	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to B\in V$$
11		simpr1	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to A\in V$$
12	1 2 3 4 5 6	ipass	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(C\in K\wedge B\in V\wedge A\in V\right)\right)\to \left(C\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A=C\underset{\dot{}}{\times }\left(B\underset{\dot{}}{,}A\right)$$
13	8 9 10 11 12	syl13anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \left(C\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A=C\underset{\dot{}}{\times }\left(B\underset{\dot{}}{,}A\right)$$
14	13	fveq2d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \underset{\dot{}}{\ast }\left(\left(C\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A\right)=\underset{\dot{}}{\ast }\left(C\underset{\dot{}}{\times }\left(B\underset{\dot{}}{,}A\right)\right)$$
15		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
16	15	adantr	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to W\in \mathrm{LMod}$$
17	3 1 5 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge C\in K\wedge B\in V\right)\to C\underset{\dot{}}{·}B\in V$$
18	16 9 10 17	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to C\underset{\dot{}}{·}B\in V$$
19	1 2 3 7	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge C\underset{\dot{}}{·}B\in V\wedge A\in V\right)\to \underset{\dot{}}{\ast }\left(\left(C\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A\right)=A\underset{\dot{}}{,}\left(C\underset{\dot{}}{·}B\right)$$
20	8 18 11 19	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \underset{\dot{}}{\ast }\left(\left(C\underset{\dot{}}{·}B\right)\underset{\dot{}}{,}A\right)=A\underset{\dot{}}{,}\left(C\underset{\dot{}}{·}B\right)$$
21	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
22	21	adantr	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to F\in \mathrm{*-Ring}$$
23	1 2 3 4	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge A\in V\right)\to B\underset{\dot{}}{,}A\in K$$
24	8 10 11 23	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to B\underset{\dot{}}{,}A\in K$$
25	7 4 6	srngmul	$$⊢\left(F\in \mathrm{*-Ring}\wedge C\in K\wedge B\underset{\dot{}}{,}A\in K\right)\to \underset{\dot{}}{\ast }\left(C\underset{\dot{}}{\times }\left(B\underset{\dot{}}{,}A\right)\right)=\underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$
26	22 9 24 25	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \underset{\dot{}}{\ast }\left(C\underset{\dot{}}{\times }\left(B\underset{\dot{}}{,}A\right)\right)=\underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$
27	14 20 26	3eqtr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{·}B\right)=\underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$
28	1 2 3 7	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge A\in V\right)\to \underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)=A\underset{\dot{}}{,}B$$
29	8 10 11 28	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)=A\underset{\dot{}}{,}B$$
30	29	oveq1d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \underset{\dot{}}{\ast }\left(B\underset{\dot{}}{,}A\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$
31	27 30	eqtrd	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to A\underset{\dot{}}{,}\left(C\underset{\dot{}}{·}B\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(C\right)$$