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	⊢ ( 𝜑 → 𝐴 ∈ No )
	muls0ord.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	muls0ord	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) = 0s ↔ ( 𝐴 = 0s ∨ 𝐵 = 0s ) ) )

Proof

Step	Hyp	Ref	Expression
1		muls0ord.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		muls0ord.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		muls02	⊢ ( 𝐵 ∈ No → ( 0s ·s 𝐵 ) = 0s )
4	2 3	syl	⊢ ( 𝜑 → ( 0s ·s 𝐵 ) = 0s )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → ( 0s ·s 𝐵 ) = 0s )
6	5	eqeq2d	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → ( ( 𝐴 ·s 𝐵 ) = ( 0s ·s 𝐵 ) ↔ ( 𝐴 ·s 𝐵 ) = 0s ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → 𝐴 ∈ No )
8		0no	⊢ 0s ∈ No
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → 0s ∈ No )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → 𝐵 ∈ No )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → 𝐵 ≠ 0s )
12	7 9 10 11	mulscan2d	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → ( ( 𝐴 ·s 𝐵 ) = ( 0s ·s 𝐵 ) ↔ 𝐴 = 0s ) )
13	6 12	bitr3d	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → ( ( 𝐴 ·s 𝐵 ) = 0s ↔ 𝐴 = 0s ) )
14	13	biimpd	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 0s ) → ( ( 𝐴 ·s 𝐵 ) = 0s → 𝐴 = 0s ) )
15	14	impancom	⊢ ( ( 𝜑 ∧ ( 𝐴 ·s 𝐵 ) = 0s ) → ( 𝐵 ≠ 0s → 𝐴 = 0s ) )
16	15	necon1bd	⊢ ( ( 𝜑 ∧ ( 𝐴 ·s 𝐵 ) = 0s ) → ( ¬ 𝐴 = 0s → 𝐵 = 0s ) )
17	16	orrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ·s 𝐵 ) = 0s ) → ( 𝐴 = 0s ∨ 𝐵 = 0s ) )
18	17	ex	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) = 0s → ( 𝐴 = 0s ∨ 𝐵 = 0s ) ) )
19		oveq1	⊢ ( 𝐴 = 0s → ( 𝐴 ·s 𝐵 ) = ( 0s ·s 𝐵 ) )
20	19	eqeq1d	⊢ ( 𝐴 = 0s → ( ( 𝐴 ·s 𝐵 ) = 0s ↔ ( 0s ·s 𝐵 ) = 0s ) )
21	4 20	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 0s → ( 𝐴 ·s 𝐵 ) = 0s ) )
22		muls01	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
23	1 22	syl	⊢ ( 𝜑 → ( 𝐴 ·s 0s ) = 0s )
24		oveq2	⊢ ( 𝐵 = 0s → ( 𝐴 ·s 𝐵 ) = ( 𝐴 ·s 0s ) )
25	24	eqeq1d	⊢ ( 𝐵 = 0s → ( ( 𝐴 ·s 𝐵 ) = 0s ↔ ( 𝐴 ·s 0s ) = 0s ) )
26	23 25	syl5ibrcom	⊢ ( 𝜑 → ( 𝐵 = 0s → ( 𝐴 ·s 𝐵 ) = 0s ) )
27	21 26	jaod	⊢ ( 𝜑 → ( ( 𝐴 = 0s ∨ 𝐵 = 0s ) → ( 𝐴 ·s 𝐵 ) = 0s ) )
28	18 27	impbid	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) = 0s ↔ ( 𝐴 = 0s ∨ 𝐵 = 0s ) ) )