vcablo

Description: Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	vcabl.1	$⊢ G = 1^{st} (W)$
	Assertion	vcablo	$⊢ W \in {CVec}_{OLD} \to G \in AbelOp$

Step	Hyp	Ref	Expression
1		vcabl.1	$⊢ G = 1^{st} (W)$
2		eqid	$⊢ 2^{nd} (W) = 2^{nd} (W)$
3		eqid	$⊢ ran G = ran G$
4	1 2 3	vciOLD	$⊢ W \in {CVec}_{OLD} \to (G \in AbelOp \land 2^{nd} (W) : ℂ \times ran G ⟶ ran G \land \forall x \in ran G (1 2^{nd} (W) x = x \land \forall y \in ℂ (\forall z \in ran G y 2^{nd} (W) (x G z) = (y 2^{nd} (W) x) G (y 2^{nd} (W) z) \land \forall z \in ℂ ((y + z) 2^{nd} (W) x = (y 2^{nd} (W) x) G (z 2^{nd} (W) x) \land y z 2^{nd} (W) x = y 2^{nd} (W) (z 2^{nd} (W) x)))))$
5	4	simp1d	$⊢ W \in {CVec}_{OLD} \to G \in AbelOp$

Metamath Proof Explorer