his52

Description: Associative law for inner product. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	his52	$⊢ (A \in ℂ \land B \in ℋ \land C \in ℋ) \to B \cdot_{ih} (\overline{A} \cdot_{ℎ} C) = A (B \cdot_{ih} C)$

Step	Hyp	Ref	Expression
1		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
2		his5	$⊢ (\overline{A} \in ℂ \land B \in ℋ \land C \in ℋ) \to B \cdot_{ih} (\overline{A} \cdot_{ℎ} C) = \overline{\overline{A}} (B \cdot_{ih} C)$
3	1 2	syl3an1	$⊢ (A \in ℂ \land B \in ℋ \land C \in ℋ) \to B \cdot_{ih} (\overline{A} \cdot_{ℎ} C) = \overline{\overline{A}} (B \cdot_{ih} C)$
4		cjcj	$⊢ A \in ℂ \to \overline{\overline{A}} = A$
5	4	oveq1d	$⊢ A \in ℂ \to \overline{\overline{A}} (B \cdot_{ih} C) = A (B \cdot_{ih} C)$
6	5	3ad2ant1	$⊢ (A \in ℂ \land B \in ℋ \land C \in ℋ) \to \overline{\overline{A}} (B \cdot_{ih} C) = A (B \cdot_{ih} C)$
7	3 6	eqtrd	$⊢ (A \in ℂ \land B \in ℋ \land C \in ℋ) \to B \cdot_{ih} (\overline{A} \cdot_{ℎ} C) = A (B \cdot_{ih} C)$

Metamath Proof Explorer