Theorem addslid

Description: Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	addslid	$$⊢A\in \mathrm{No}\to 0_s{+}_{s}A=A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
2		0sno	$$⊢0_s\in \mathrm{No}$$
3	2	a1i	$$⊢A\in \mathrm{No}\to 0_s\in \mathrm{No}$$
4	1 3	addscomd	$$⊢A\in \mathrm{No}\to A{+}_s{0}_s=0_s{+}_{s}A$$
5		addsrid	$$⊢A\in \mathrm{No}\to A{+}_s{0}_s=A$$
6	4 5	eqtr3d	$$⊢A\in \mathrm{No}\to 0_s{+}_{s}A=A$$