Theorem negsdi

Description: Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025)

	Ref	Expression
Assertion	negsdi	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( -us ` ( A +s B ) ) = ( ( -us ` A ) +s ( -us ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addscl	Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No ) with typecode |-
2	1	negsidd	Could not format ( ( A e. No /\ B e. No ) -> ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = 0s ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = 0s ) with typecode |-
3		negsid	Could not format ( A e. No -> ( A +s ( -us ` A ) ) = 0s ) : No typesetting found for |- ( A e. No -> ( A +s ( -us ` A ) ) = 0s ) with typecode |-
4		negsid	Could not format ( B e. No -> ( B +s ( -us ` B ) ) = 0s ) : No typesetting found for |- ( B e. No -> ( B +s ( -us ` B ) ) = 0s ) with typecode |-
5	3 4	oveqan12d	Could not format ( ( A e. No /\ B e. No ) -> ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) = ( 0s +s 0s ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) = ( 0s +s 0s ) ) with typecode |-
6		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
7		addslid	Could not format ( 0s e. No -> ( 0s +s 0s ) = 0s ) : No typesetting found for |- ( 0s e. No -> ( 0s +s 0s ) = 0s ) with typecode |-
8	6 7	ax-mp	Could not format ( 0s +s 0s ) = 0s : No typesetting found for |- ( 0s +s 0s ) = 0s with typecode |-
9	5 8	eqtr2di	Could not format ( ( A e. No /\ B e. No ) -> 0s = ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> 0s = ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) ) with typecode |-
10		simpl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \mathrm{No}$$
11	10	negscld	Could not format ( ( A e. No /\ B e. No ) -> ( -us ` A ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( -us ` A ) e. No ) with typecode |-
12		simpr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \mathrm{No}$$
13	12	negscld	Could not format ( ( A e. No /\ B e. No ) -> ( -us ` B ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( -us ` B ) e. No ) with typecode |-
14	10 11 12 13	adds4d	Could not format ( ( A e. No /\ B e. No ) -> ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( A +s ( -us ` A ) ) +s ( B +s ( -us ` B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) ) with typecode |-
15	2 9 14	3eqtrd	Could not format ( ( A e. No /\ B e. No ) -> ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) ) with typecode |-
16	1	negscld	Could not format ( ( A e. No /\ B e. No ) -> ( -us ` ( A +s B ) ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( -us ` ( A +s B ) ) e. No ) with typecode |-
17		negscl	Could not format ( A e. No -> ( -us ` A ) e. No ) : No typesetting found for |- ( A e. No -> ( -us ` A ) e. No ) with typecode |-
18		negscl	Could not format ( B e. No -> ( -us ` B ) e. No ) : No typesetting found for |- ( B e. No -> ( -us ` B ) e. No ) with typecode |-
19		addscl	Could not format ( ( ( -us ` A ) e. No /\ ( -us ` B ) e. No ) -> ( ( -us ` A ) +s ( -us ` B ) ) e. No ) : No typesetting found for |- ( ( ( -us ` A ) e. No /\ ( -us ` B ) e. No ) -> ( ( -us ` A ) +s ( -us ` B ) ) e. No ) with typecode |-
20	17 18 19	syl2an	Could not format ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) +s ( -us ` B ) ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) +s ( -us ` B ) ) e. No ) with typecode |-
21	16 20 1	addscan1d	Could not format ( ( A e. No /\ B e. No ) -> ( ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) <-> ( -us ` ( A +s B ) ) = ( ( -us ` A ) +s ( -us ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( ( A +s B ) +s ( -us ` ( A +s B ) ) ) = ( ( A +s B ) +s ( ( -us ` A ) +s ( -us ` B ) ) ) <-> ( -us ` ( A +s B ) ) = ( ( -us ` A ) +s ( -us ` B ) ) ) ) with typecode |-
22	15 21	mpbid	Could not format ( ( A e. No /\ B e. No ) -> ( -us ` ( A +s B ) ) = ( ( -us ` A ) +s ( -us ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( -us ` ( A +s B ) ) = ( ( -us ` A ) +s ( -us ` B ) ) ) with typecode |-