Axiom ax-hvaddid 10506

Description: Addition with the zero vector.

Assertion

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

Detailed syntax breakdown of Axiom ax-hvaddid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 10420	. . 3 class ~H
3	1, 2	wcel 1300	. 2 wff A e. ~H
4		c0v 10423	. . . 4 class 0h
5		cva 10421	. . . 4 class +h
6	1, 4, 5	co 4884	. . 3 class (A +h 0h)
7	6, 1	wceq 1298	. 2 wff (A +h 0h) = A
8	3, 7	wi 3	1 wff (A e. ~H -> (A +h 0h) = A)

This axiom is referenced by:  hvaddid2 10524  hvpncan 10540  hvsubeq0i 10562  hvsubcan2i 10563  hvsubaddi 10565  hvsub0 10576  hvaddsub4 10578  norm3difi 10647  chocunii 10805  pjthlem14 10865  omlsilem 10877  pjoc1i 10897  pjchi 10898  shsel1 10918  shunssi 10970  spansncvi 11232  5oalem1 11234  5oalem2 11235  3oalem2 11243  pjssmii 11261  pjvi 11285  hoaddid1i 11349  lnop0 11527  lnopmul 11528  lnfn0i 11608  lnfnmuli 11610  pjclem4 11772  pj3si 11780  hst1h 11799  sumdmdlem 11990

Copyright terms: Public domain