Metamath Proof Explorer

Theorem nvmfval

Description: Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvmval.1	$⊢ X = BaseSet (U)$
		nvmval.2	$⊢ G = +_{v} (U)$
		nvmval.4	$⊢ S = \cdot_{𝑠OLD} (U)$
		nvmval.3	$⊢ M = -_{v} (U)$
	Assertion	nvmfval	$⊢ U \in NrmCVec \to M = (x \in X, y \in X ⟼ x G (-1 S y))$

Proof

Step	Hyp	Ref	Expression
1		nvmval.1	$⊢ X = BaseSet (U)$
2		nvmval.2	$⊢ G = +_{v} (U)$
3		nvmval.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		nvmval.3	$⊢ M = -_{v} (U)$
5	2	nvgrp	$⊢ U \in NrmCVec \to G \in GrpOp$
6	1 2	bafval	$⊢ X = ran G$
7		eqid	$⊢ inv (G) = inv (G)$
8	2 4	vsfval	$⊢ M = /_{g} (G)$
9	6 7 8	grpodivfval	$⊢ G \in GrpOp \to M = (x \in X, y \in X ⟼ x G inv (G) (y))$
10	5 9	syl	$⊢ U \in NrmCVec \to M = (x \in X, y \in X ⟼ x G inv (G) (y))$
11	1 2 3 7	nvinv	$⊢ (U \in NrmCVec \land y \in X) \to -1 S y = inv (G) (y)$
12	11	3adant2	$⊢ (U \in NrmCVec \land x \in X \land y \in X) \to -1 S y = inv (G) (y)$
13	12	oveq2d	$⊢ (U \in NrmCVec \land x \in X \land y \in X) \to x G (-1 S y) = x G inv (G) (y)$
14	13	mpoeq3dva	$⊢ U \in NrmCVec \to (x \in X, y \in X ⟼ x G (-1 S y)) = (x \in X, y \in X ⟼ x G inv (G) (y))$
15	10 14	eqtr4d	$⊢ U \in NrmCVec \to M = (x \in X, y \in X ⟼ x G (-1 S y))$