Theorem hvaddid2t 8813

Description: Addition with the zero vector.

Assertion

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

Proof of Theorem hvaddid2t

Step	Hyp	Ref	Expression
1		ax-hv0cl 8794	. . 3 |- 0h e. H~
2		ax-hvcom 8792	. . 3 |- ((A e. H~ /\ 0h e. H~) -> (A +h 0h) = (0h +h A))
3	1, 2	mpan2 694	. 2 |- (A e. H~ -> (A +h 0h) = (0h +h A))
4		ax-hvaddid 8795	. 2 |- (A e. H~ -> (A +h 0h) = A)
5	3, 4	eqtr3d 1501	1 |- (A e. H~ -> (0h +h A) = A)

Syntax hints:   -> wi 3   = wceq 953   e. wcel 955  (class class class)co 3948  H~chil 8727   +h cva 8728  0hc0v 8730

This theorem is referenced by:  hv2negt 8818  hvaddid2 8819  hvaddsub4t 8866  hilabl 8948  hilid 8949  chocuni 9088  shunss 9252  spanunsn 9419  5oalem2 9517  3oalem2 9525

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452  ax-hvcom 8792  ax-hv0cl 8794  ax-hvaddid 8795

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

Copyright terms: Public domain