Theorem mulscan2d

Description: Cancellation of surreal multiplication when the right term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	mulscan2d.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulscan2d.2	$$⊢\phi \to B\in \mathrm{No}$$
	mulscan2d.3	$$⊢\phi \to C\in \mathrm{No}$$
	mulscan2d.4	No typesetting found for |- ( ph -> C =/= 0s ) with typecode |-
Assertion	mulscan2d	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulscan2d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulscan2d.2	$$⊢\phi \to B\in \mathrm{No}$$
3		mulscan2d.3	$$⊢\phi \to C\in \mathrm{No}$$
4		mulscan2d.4	Could not format ( ph -> C =/= 0s ) : No typesetting found for |- ( ph -> C =/= 0s ) with typecode |-
5		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
6		sltneg	Could not format ( ( C e. No /\ 0s e. No ) -> ( C ( -us ` 0s ) ( C ( -us ` 0s )
7	3 5 6	sylancl	Could not format ( ph -> ( C ( -us ` 0s ) ( C ( -us ` 0s )
8		negs0s	Could not format ( -us ` 0s ) = 0s : No typesetting found for |- ( -us ` 0s ) = 0s with typecode |-
9	8	breq1i	Could not format ( ( -us ` 0s ) 0s 0s
10	7 9	bitrdi	Could not format ( ph -> ( C 0s ( C 0s
11	1 3	mulnegs2d	Could not format ( ph -> ( A x.s ( -us ` C ) ) = ( -us ` ( A x.s C ) ) ) : No typesetting found for |- ( ph -> ( A x.s ( -us ` C ) ) = ( -us ` ( A x.s C ) ) ) with typecode |-
12	2 3	mulnegs2d	Could not format ( ph -> ( B x.s ( -us ` C ) ) = ( -us ` ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( B x.s ( -us ` C ) ) = ( -us ` ( B x.s C ) ) ) with typecode |-
13	11 12	eqeq12d	Could not format ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) ) ) with typecode |-
14	1 3	mulscld	Could not format ( ph -> ( A x.s C ) e. No ) : No typesetting found for |- ( ph -> ( A x.s C ) e. No ) with typecode |-
15	2 3	mulscld	Could not format ( ph -> ( B x.s C ) e. No ) : No typesetting found for |- ( ph -> ( B x.s C ) e. No ) with typecode |-
16		negs11	Could not format ( ( ( A x.s C ) e. No /\ ( B x.s C ) e. No ) -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) : No typesetting found for |- ( ( ( A x.s C ) e. No /\ ( B x.s C ) e. No ) -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) with typecode |-
17	14 15 16	syl2anc	Could not format ( ph -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) with typecode |-
18	13 17	bitrd	Could not format ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) with typecode |-
19	18	adantr	Could not format ( ( ph /\ 0s ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ 0s ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) ) with typecode |-
20	1	adantr	Could not format ( ( ph /\ 0s A e. No ) : No typesetting found for |- ( ( ph /\ 0s A e. No ) with typecode |-
21	2	adantr	Could not format ( ( ph /\ 0s B e. No ) : No typesetting found for |- ( ( ph /\ 0s B e. No ) with typecode |-
22	3	negscld	Could not format ( ph -> ( -us ` C ) e. No ) : No typesetting found for |- ( ph -> ( -us ` C ) e. No ) with typecode |-
23	22	adantr	Could not format ( ( ph /\ 0s ( -us ` C ) e. No ) : No typesetting found for |- ( ( ph /\ 0s ( -us ` C ) e. No ) with typecode |-
24		simpr	Could not format ( ( ph /\ 0s 0s 0s
25	20 21 23 24	mulscan2dlem	Could not format ( ( ph /\ 0s ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> A = B ) ) : No typesetting found for |- ( ( ph /\ 0s ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> A = B ) ) with typecode |-
26	19 25	bitr3d	Could not format ( ( ph /\ 0s ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) : No typesetting found for |- ( ( ph /\ 0s ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) with typecode |-
27	10 26	sylbida	Could not format ( ( ph /\ C ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) : No typesetting found for |- ( ( ph /\ C ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) with typecode |-
28	1	adantr	Could not format ( ( ph /\ 0s A e. No ) : No typesetting found for |- ( ( ph /\ 0s A e. No ) with typecode |-
29	2	adantr	Could not format ( ( ph /\ 0s B e. No ) : No typesetting found for |- ( ( ph /\ 0s B e. No ) with typecode |-
30	3	adantr	Could not format ( ( ph /\ 0s C e. No ) : No typesetting found for |- ( ( ph /\ 0s C e. No ) with typecode |-
31		simpr	Could not format ( ( ph /\ 0s 0s 0s
32	28 29 30 31	mulscan2dlem	Could not format ( ( ph /\ 0s ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) : No typesetting found for |- ( ( ph /\ 0s ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) with typecode |-
33		slttrine	Could not format ( ( C e. No /\ 0s e. No ) -> ( C =/= 0s <-> ( C ( C =/= 0s <-> ( C
34	3 5 33	sylancl	Could not format ( ph -> ( C =/= 0s <-> ( C ( C =/= 0s <-> ( C
35	4 34	mpbid	Could not format ( ph -> ( C ( C
36	27 32 35	mpjaodan	Could not format ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) : No typesetting found for |- ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) ) with typecode |-