Metamath Proof Explorer


Theorem vc0rid

Description: The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses vczcl.1 𝐺 = ( 1st𝑊 )
vczcl.2 𝑋 = ran 𝐺
vczcl.3 𝑍 = ( GId ‘ 𝐺 )
Assertion vc0rid ( ( 𝑊 ∈ CVecOLD𝐴𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 vczcl.1 𝐺 = ( 1st𝑊 )
2 vczcl.2 𝑋 = ran 𝐺
3 vczcl.3 𝑍 = ( GId ‘ 𝐺 )
4 1 vcgrp ( 𝑊 ∈ CVecOLD𝐺 ∈ GrpOp )
5 2 3 grporid ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 )
6 4 5 sylan ( ( 𝑊 ∈ CVecOLD𝐴𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 )