Theorem muls0ord

Description: If a surreal product is zero, one of its factors must be zero. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Hypotheses	muls0ord.1	|- ( ph -> A e. No )
	muls0ord.2	|- ( ph -> B e. No )
Assertion	muls0ord	|- ( ph -> ( ( A x.s B ) = 0s <-> ( A = 0s \/ B = 0s ) ) )

Proof

Step	Hyp	Ref	Expression
1		muls0ord.1	|- ( ph -> A e. No )
2		muls0ord.2	|- ( ph -> B e. No )
3		muls02	|- ( B e. No -> ( 0s x.s B ) = 0s )
4	2 3	syl	|- ( ph -> ( 0s x.s B ) = 0s )
5	4	adantr	|- ( ( ph /\ B =/= 0s ) -> ( 0s x.s B ) = 0s )
6	5	eqeq2d	|- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> ( A x.s B ) = 0s ) )
7	1	adantr	|- ( ( ph /\ B =/= 0s ) -> A e. No )
8		0sno	|- 0s e. No
9	8	a1i	|- ( ( ph /\ B =/= 0s ) -> 0s e. No )
10	2	adantr	|- ( ( ph /\ B =/= 0s ) -> B e. No )
11		simpr	|- ( ( ph /\ B =/= 0s ) -> B =/= 0s )
12	7 9 10 11	mulscan2d	|- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = ( 0s x.s B ) <-> A = 0s ) )
13	6 12	bitr3d	|- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s <-> A = 0s ) )
14	13	biimpd	|- ( ( ph /\ B =/= 0s ) -> ( ( A x.s B ) = 0s -> A = 0s ) )
15	14	impancom	|- ( ( ph /\ ( A x.s B ) = 0s ) -> ( B =/= 0s -> A = 0s ) )
16	15	necon1bd	|- ( ( ph /\ ( A x.s B ) = 0s ) -> ( -. A = 0s -> B = 0s ) )
17	16	orrd	|- ( ( ph /\ ( A x.s B ) = 0s ) -> ( A = 0s \/ B = 0s ) )
18	17	ex	|- ( ph -> ( ( A x.s B ) = 0s -> ( A = 0s \/ B = 0s ) ) )
19		oveq1	|- ( A = 0s -> ( A x.s B ) = ( 0s x.s B ) )
20	19	eqeq1d	|- ( A = 0s -> ( ( A x.s B ) = 0s <-> ( 0s x.s B ) = 0s ) )
21	4 20	syl5ibrcom	|- ( ph -> ( A = 0s -> ( A x.s B ) = 0s ) )
22		muls01	|- ( A e. No -> ( A x.s 0s ) = 0s )
23	1 22	syl	|- ( ph -> ( A x.s 0s ) = 0s )
24		oveq2	|- ( B = 0s -> ( A x.s B ) = ( A x.s 0s ) )
25	24	eqeq1d	|- ( B = 0s -> ( ( A x.s B ) = 0s <-> ( A x.s 0s ) = 0s ) )
26	23 25	syl5ibrcom	|- ( ph -> ( B = 0s -> ( A x.s B ) = 0s ) )
27	21 26	jaod	|- ( ph -> ( ( A = 0s \/ B = 0s ) -> ( A x.s B ) = 0s ) )
28	18 27	impbid	|- ( ph -> ( ( A x.s B ) = 0s <-> ( A = 0s \/ B = 0s ) ) )