Description: Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | vcabl.1 | ⊢ 𝐺 = ( 1st ‘ 𝑊 ) | |
Assertion | vcablo | ⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vcabl.1 | ⊢ 𝐺 = ( 1st ‘ 𝑊 ) | |
2 | eqid | ⊢ ( 2nd ‘ 𝑊 ) = ( 2nd ‘ 𝑊 ) | |
3 | eqid | ⊢ ran 𝐺 = ran 𝐺 | |
4 | 1 2 3 | vciOLD | ⊢ ( 𝑊 ∈ CVecOLD → ( 𝐺 ∈ AbelOp ∧ ( 2nd ‘ 𝑊 ) : ( ℂ × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ( ( 1 ( 2nd ‘ 𝑊 ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 ( 2nd ‘ 𝑊 ) ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 ( 2nd ‘ 𝑊 ) 𝑥 ) 𝐺 ( 𝑦 ( 2nd ‘ 𝑊 ) 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) ( 2nd ‘ 𝑊 ) 𝑥 ) = ( ( 𝑦 ( 2nd ‘ 𝑊 ) 𝑥 ) 𝐺 ( 𝑧 ( 2nd ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) ( 2nd ‘ 𝑊 ) 𝑥 ) = ( 𝑦 ( 2nd ‘ 𝑊 ) ( 𝑧 ( 2nd ‘ 𝑊 ) 𝑥 ) ) ) ) ) ) ) |
5 | 4 | simp1d | ⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp ) |