Metamath Proof Explorer

Theorem nvscom

Description: Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvscl.1	$⊢ X = BaseSet (U)$
		nvscl.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	Assertion	nvscom	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A S (B S C) = B S (A S C)$

Proof

Step	Hyp	Ref	Expression
1		nvscl.1	$⊢ X = BaseSet (U)$
2		nvscl.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
4	3	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to A B S C = B A S C$
5	4	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land C \in X) \to A B S C = B A S C$
6	5	adantl	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A B S C = B A S C$
7	1 2	nvsass	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A B S C = A S (B S C)$
8		3ancoma	$⊢ (A \in ℂ \land B \in ℂ \land C \in X) \leftrightarrow (B \in ℂ \land A \in ℂ \land C \in X)$
9	1 2	nvsass	$⊢ (U \in NrmCVec \land (B \in ℂ \land A \in ℂ \land C \in X)) \to B A S C = B S (A S C)$
10	8 9	sylan2b	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to B A S C = B S (A S C)$
11	6 7 10	3eqtr3d	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in ℂ \land C \in X)) \to A S (B S C) = B S (A S C)$