Theorem no2times

Description: Version of 2times for surreal numbers. (Contributed by Scott Fenton, 23-Jul-2025)

	Ref	Expression
Assertion	no2times	Could not format assertion : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
2	1	oveq1i	Could not format ( ( 1s +s 1s ) x.s A ) = ( 2s x.s A ) : No typesetting found for |- ( ( 1s +s 1s ) x.s A ) = ( 2s x.s A ) with typecode |-
3	2	eqcomi	Could not format ( 2s x.s A ) = ( ( 1s +s 1s ) x.s A ) : No typesetting found for |- ( 2s x.s A ) = ( ( 1s +s 1s ) x.s A ) with typecode |-
4		1sno	$$⊢1_s\in \mathrm{No}$$
5	4	a1i	$$⊢A\in \mathrm{No}\to 1_s\in \mathrm{No}$$
6		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
7	5 5 6	addsdird	$$⊢A\in \mathrm{No}\to \left(1_s{+}_s{1}_s\right){\cdot }_{s}A=\left(1_s{\cdot }_{s}A\right){+}_s\left(1_s{\cdot }_{s}A\right)$$
8		mulslid	$$⊢A\in \mathrm{No}\to 1_s{\cdot }_{s}A=A$$
9	8 8	oveq12d	$$⊢A\in \mathrm{No}\to \left(1_s{\cdot }_{s}A\right){+}_s\left(1_s{\cdot }_{s}A\right)=A{+}_{s}A$$
10	7 9	eqtrd	$$⊢A\in \mathrm{No}\to \left(1_s{+}_s{1}_s\right){\cdot }_{s}A=A{+}_{s}A$$
11	3 10	eqtrid	Could not format ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-