cphass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. See ipass , his5 . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphipcj.v	$⊢ V = {Base}_{W}$
	cphass.f	$⊢ F = Scalar (W)$
	cphass.k	$⊢ K = {Base}_{F}$
	cphass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	cphass	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A (B \underset{˙}{,} C)$

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3		cphass.f	$⊢ F = Scalar (W)$
4		cphass.k	$⊢ K = {Base}_{F}$
5		cphass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
7		eqid	$⊢ \cdot_{F} = \cdot_{F}$
8	3 1 2 4 5 7	ipass	$⊢ (W \in PreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A \cdot_{F} (B \underset{˙}{,} C)$
9	6 8	sylan	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A \cdot_{F} (B \underset{˙}{,} C)$
10		cphclm	$⊢ W \in CPreHil \to W \in CMod$
11	3	clmmul	$⊢ W \in CMod \to \times = \cdot_{F}$
12	10 11	syl	$⊢ W \in CPreHil \to \times = \cdot_{F}$
13	12	adantr	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to \times = \cdot_{F}$
14	13	oveqd	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to A (B \underset{˙}{,} C) = A \cdot_{F} (B \underset{˙}{,} C)$
15	9 14	eqtr4d	$⊢ (W \in CPreHil \land (A \in K \land B \in V \land C \in V)) \to (A \underset{˙}{\cdot} B) \underset{˙}{,} C = A (B \underset{˙}{,} C)$

Metamath Proof Explorer