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

Metamath Proof Explorer

Theorem vczcl

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

Ref Expression
Hypotheses vczcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑊 )
vczcl.2 ⊢ 𝑋 = ran 𝐺
vczcl.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion vczcl ( 𝑊 ∈ 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 grpoidcl ⊢ ( 𝐺 ∈ GrpOp → 𝑍 ∈ 𝑋 )
6 4 5 syl ⊢ ( 𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋 )