Theorem hvaddlid

Description: Addition with the zero vector. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hvaddlid	$$⊢A\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}A=A$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		ax-hvcom	$$⊢\left(A\in \mathscr{H}\wedge 0_{ℎ}\in \mathscr{H}\right)\to A{+}_{ℎ}{0}_{ℎ}=0_{ℎ}{+}_{ℎ}A$$
3	1 2	mpan2	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=0_{ℎ}{+}_{ℎ}A$$
4		ax-hvaddid	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=A$$
5	3 4	eqtr3d	$$⊢A\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}A=A$$