Theorem hvaddid2 10524

Description: Addition with the zero vector.

Assertion

Ref	Expression
hvaddid2	|- (A e. ~H -> (0h +h A) = A)

Proof of Theorem hvaddid2

Step	Hyp	Ref	Expression
1		ax-hv0cl 10505	. . 3 |- 0h e. ~H
2		ax-hvcom 10503	. . 3 |- ((A e. ~H /\ 0h e. ~H) -> (A +h 0h) = (0h +h A))
3	1, 2	mpan2 760	. 2 |- (A e. ~H -> (A +h 0h) = (0h +h A))
4		ax-hvaddid 10506	. 2 |- (A e. ~H -> (A +h 0h) = A)
5	3, 4	eqtr3d 1927	1 |- (A e. ~H -> (0h +h A) = A)

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300  (class class class)co 4884  ~Hchil 10420   +h cva 10421  0hc0v 10423

This theorem is referenced by:  hv2neg 10529  hvaddid2i 10530  hvaddsub4 10578  hilabl 10660  hilid 10661  chocunii 10805  shunssi 10970  spanunsni 11135  5oalem2 11235  3oalem2 11243

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865  ax-hvcom 10503  ax-hv0cl 10505  ax-hvaddid 10506

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain