Theorem hvaddid2 8893

Description: Addition with the zero vector.

Hypothesis

Ref	Expression
hvaddid2.1	|- A e. H~

Assertion

Ref	Expression
hvaddid2	|- (0h +h A) = A

Proof of Theorem hvaddid2

Step	Hyp	Ref	Expression
1		hvaddid2.1	. 2 |- A e. H~
2		hvaddid2t 8887	. 2 |- (A e. H~ -> (0h +h A) = A)
3	1, 2	ax-mp 7	1 |- (0h +h A) = A

Syntax hints:   = wceq 958   e. wcel 960  (class class class)co 3969  H~chil 8783   +h cva 8784  0hc0v 8786

This theorem is referenced by:  hvsubeq0 8925  hvaddcan 8927  hsn0elch 9115  hhssnv 9129  shscl 9276

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462  ax-hvcom 8866  ax-hv0cl 8868  ax-hvaddid 8869

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472

Copyright terms: Public domain