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

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 ∈ NrmCVec ∧ A ∈ X → 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 ∈ NrmCVec → Z = GId ⁡ G
5 4 oveq1d ⊢ U ∈ NrmCVec → Z G A = GId ⁡ G G A
6 5 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → Z G A = GId ⁡ G G A
7 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
8 1 2 bafval ⊢ X = ran ⁡ G
9 eqid ⊢ GId ⁡ G = GId ⁡ G
10 8 9 grpolid ⊢ G ∈ GrpOp ∧ A ∈ X → GId ⁡ G G A = A
11 7 10 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X → GId ⁡ G G A = A
12 6 11 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → Z G A = A