Metamath Proof Explorer

Theorem nv0rid

Description: The zero vector is a right identity element. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nv0id.1	$⊢ X = BaseSet (U)$
		nv0id.2	$⊢ G = +_{v} (U)$
		nv0id.6	$⊢ Z = 0_{vec} (U)$
	Assertion	nv0rid	$⊢ (U \in NrmCVec \land A \in X) \to A G Z = A$

Proof

Step	Hyp	Ref	Expression
1		nv0id.1	$⊢ X = BaseSet (U)$
2		nv0id.2	$⊢ G = +_{v} (U)$
3		nv0id.6	$⊢ Z = 0_{vec} (U)$
4	2 3	0vfval	$⊢ U \in NrmCVec \to Z = GId (G)$
5	4	oveq2d	$⊢ U \in NrmCVec \to A G Z = A G GId (G)$
6	5	adantr	$⊢ (U \in NrmCVec \land A \in X) \to A G Z = A G GId (G)$
7	2	nvgrp	$⊢ U \in NrmCVec \to G \in GrpOp$
8	1 2	bafval	$⊢ X = ran G$
9		eqid	$⊢ GId (G) = GId (G)$
10	8 9	grporid	$⊢ (G \in GrpOp \land A \in X) \to A G GId (G) = A$
11	7 10	sylan	$⊢ (U \in NrmCVec \land A \in X) \to A G GId (G) = A$
12	6 11	eqtrd	$⊢ (U \in NrmCVec \land A \in X) \to A G Z = A$