This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvinv

Description: Minus 1 times a vector is the underlying group's inverse element. Equation 2 of Kreyszig p. 51. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvinv.1	$⊢ X = BaseSet (U)$
		nvinv.2	$⊢ G = +_{v} (U)$
		nvinv.4	$⊢ S = \cdot_{𝑠OLD} (U)$
		nvinv.5	$⊢ M = inv (G)$
	Assertion	nvinv	$⊢ (U \in NrmCVec \land A \in X) \to -1 S A = M (A)$

Proof

Step	Hyp	Ref	Expression
1		nvinv.1	$⊢ X = BaseSet (U)$
2		nvinv.2	$⊢ G = +_{v} (U)$
3		nvinv.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		nvinv.5	$⊢ M = inv (G)$
5		eqid	$⊢ 1^{st} (U) = 1^{st} (U)$
6	5	nvvc	$⊢ U \in NrmCVec \to 1^{st} (U) \in {CVec}_{OLD}$
7	2	vafval	$⊢ G = 1^{st} (1^{st} (U))$
8	3	smfval	$⊢ S = 2^{nd} (1^{st} (U))$
9	1 2	bafval	$⊢ X = ran G$
10	7 8 9 4	vcm	$⊢ (1^{st} (U) \in {CVec}_{OLD} \land A \in X) \to -1 S A = M (A)$
11	6 10	sylan	$⊢ (U \in NrmCVec \land A \in X) \to -1 S A = M (A)$