Metamath Proof Explorer

Theorem vc2OLD

Description: A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007) Obsolete theorem, use clmvs2 together with cvsclm instead. (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	vciOLD.1	$⊢ G = 1^{st} (W)$
		vciOLD.2	$⊢ S = 2^{nd} (W)$
		vciOLD.3	$⊢ X = ran G$
	Assertion	vc2OLD	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to A G A = 2 S A$

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	$⊢ G = 1^{st} (W)$
2		vciOLD.2	$⊢ S = 2^{nd} (W)$
3		vciOLD.3	$⊢ X = ran G$
4	1 2 3	vcidOLD	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to 1 S A = A$
5	4 4	oveq12d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (1 S A) G (1 S A) = A G A$
6		df-2	$⊢ 2 = 1 + 1$
7	6	oveq1i	$⊢ 2 S A = (1 + 1) S A$
8		ax-1cn	$⊢ 1 \in ℂ$
9	1 2 3	vcdir	$⊢ (W \in {CVec}_{OLD} \land (1 \in ℂ \land 1 \in ℂ \land A \in X)) \to (1 + 1) S A = (1 S A) G (1 S A)$
10	8 9	mp3anr1	$⊢ (W \in {CVec}_{OLD} \land (1 \in ℂ \land A \in X)) \to (1 + 1) S A = (1 S A) G (1 S A)$
11	8 10	mpanr1	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (1 + 1) S A = (1 S A) G (1 S A)$
12	7 11	eqtr2id	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to (1 S A) G (1 S A) = 2 S A$
13	5 12	eqtr3d	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to A G A = 2 S A$