Metamath Proof Explorer

Theorem nv0lid

Description: The zero vector is a left 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	nv0lid	$⊢ (U \in NrmCVec \land A \in X) \to Z G A = 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	oveq1d	$⊢ U \in NrmCVec \to Z G A = GId (G) G A$
6	5	adantr	$⊢ (U \in NrmCVec \land A \in X) \to Z G A = GId (G) G A$
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	grpolid	$⊢ (G \in GrpOp \land A \in X) \to GId (G) G A = A$
11	7 10	sylan	$⊢ (U \in NrmCVec \land A \in X) \to GId (G) G A = A$
12	6 11	eqtrd	$⊢ (U \in NrmCVec \land A \in X) \to Z G A = A$