dipassr2

Description: "Associative" law for inner product. Conjugate version of dipassr . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipass.1	$⊢ X = BaseSet (U)$
	ipass.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	ipass.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	dipassr2	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to A P (\overline{B} S C) = B (A P C)$

Step	Hyp	Ref	Expression
1		ipass.1	$⊢ X = BaseSet (U)$
2		ipass.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		ipass.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		cjcl	$⊢ B \in ℂ \to \overline{B} \in ℂ$
5	1 2 3	dipassr	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land \overline{B} \in ℂ \land C \in X)) \to A P (\overline{B} S C) = \overline{\overline{B}} (A P C)$
6	4 5	syl3anr2	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to A P (\overline{B} S C) = \overline{\overline{B}} (A P C)$
7		cjcj	$⊢ B \in ℂ \to \overline{\overline{B}} = B$
8	7	3ad2ant2	$⊢ (A \in X \land B \in ℂ \land C \in X) \to \overline{\overline{B}} = B$
9	8	adantl	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{\overline{B}} = B$
10	9	oveq1d	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{\overline{B}} (A P C) = B (A P C)$
11	6 10	eqtrd	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to A P (\overline{B} S C) = B (A P C)$

Metamath Proof Explorer