cphassir

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

	Ref	Expression
Hypotheses	cphassi.x	$⊢ X = {Base}_{W}$
	cphassi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	cphassi.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphassi.f	$⊢ F = Scalar (W)$
	cphassi.k	$⊢ K = {Base}_{F}$
Assertion	cphassir	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) = (- i) (A \underset{˙}{,} B)$

Step	Hyp	Ref	Expression
1		cphassi.x	$⊢ X = {Base}_{W}$
2		cphassi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		cphassi.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
4		cphassi.f	$⊢ F = Scalar (W)$
5		cphassi.k	$⊢ K = {Base}_{F}$
6		simp1l	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to W \in CPreHil$
7		simp1r	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to i \in K$
8		simp2	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \in X$
9		simp3	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to B \in X$
10	3 1 4 5 2	cphassr	$⊢ (W \in CPreHil \land (i \in K \land A \in X \land B \in X)) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) = \overline{i} (A \underset{˙}{,} B)$
11	6 7 8 9 10	syl13anc	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) = \overline{i} (A \underset{˙}{,} B)$
12		cji	$⊢ \overline{i} = - i$
13	12	oveq1i	$⊢ \overline{i} (A \underset{˙}{,} B) = (- i) (A \underset{˙}{,} B)$
14	11 13	eqtrdi	$⊢ ((W \in CPreHil \land i \in K) \land A \in X \land B \in X) \to A \underset{˙}{,} (i \underset{˙}{\cdot} B) = (- i) (A \underset{˙}{,} B)$

Metamath Proof Explorer