homul12

Description: Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	homul12	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to A \cdot_{op} (B \cdot_{op} T) = B \cdot_{op} (A \cdot_{op} T)$

Step	Hyp	Ref	Expression
1		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
2	1	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to A B \cdot_{op} T = B A \cdot_{op} T$
3	2	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to A B \cdot_{op} T = B A \cdot_{op} T$
4		homulass	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to A B \cdot_{op} T = A \cdot_{op} (B \cdot_{op} T)$
5		homulass	$⊢ (B \in ℂ \land A \in ℂ \land T : ℋ ⟶ ℋ) \to B A \cdot_{op} T = B \cdot_{op} (A \cdot_{op} T)$
6	5	3com12	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to B A \cdot_{op} T = B \cdot_{op} (A \cdot_{op} T)$
7	3 4 6	3eqtr3d	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to A \cdot_{op} (B \cdot_{op} T) = B \cdot_{op} (A \cdot_{op} T)$

Metamath Proof Explorer