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 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 ) |
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 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑍 ) = 𝐴 ) |