Theorem ipassr2

Description: "Associative" law for inner product. Conjugate version of ipassr . (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	ipassr2	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }C=A\underset{\dot{}}{,}\left(\underset{\dot{}}{\ast }\left(C\right)\underset{\dot{}}{·}B\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		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$$
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	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
12		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$$
13	7 4	srngcl	$$⊢\left(F\in \mathrm{*-Ring}\wedge C\in K\right)\to \underset{\dot{}}{\ast }\left(C\right)\in K$$
14	11 12 13	syl2an2r	$$⊢\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\right)\in K$$
15	1 2 3 4 5 6 7	ipassr	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge \underset{\dot{}}{\ast }\left(C\right)\in K\right)\right)\to A\underset{\dot{}}{,}\left(\underset{\dot{}}{\ast }\left(C\right)\underset{\dot{}}{·}B\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(C\right)\right)$$
16	8 9 10 14 15	syl13anc	$$⊢\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(\underset{\dot{}}{\ast }\left(C\right)\underset{\dot{}}{·}B\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(C\right)\right)$$
17	7 4	srngnvl	$$⊢\left(F\in \mathrm{*-Ring}\wedge C\in K\right)\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(C\right)\right)=C$$
18	11 12 17	syl2an2r	$$⊢\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(\underset{\dot{}}{\ast }\left(C\right)\right)=C$$
19	18	oveq2d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }\underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(C\right)\right)=\left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }C$$
20	16 19	eqtr2d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in K\right)\right)\to \left(A\underset{\dot{}}{,}B\right)\underset{\dot{}}{\times }C=A\underset{\dot{}}{,}\left(\underset{\dot{}}{\ast }\left(C\right)\underset{\dot{}}{·}B\right)$$