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

Metamath Proof Explorer

Theorem nv2

Description: A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008) (New usage is discouraged.)

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

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