Theorem divsmulw

Description: Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex , we can eliminate the existence hypothesis (see divsmul ). (Contributed by Scott Fenton, 12-Mar-2025)

	Ref	Expression
Assertion	divsmulw	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		divsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) → ( 𝐴 /su 𝐶 ) = ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) )
2	1	eqeq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
3	2	3expb	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
6		simpl2	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → 𝐵 ∈ No )
7		simp3l	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → 𝐶 ∈ No )
8		simp3r	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → 𝐶 ≠ 0s )
9		simp1	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → 𝐴 ∈ No )
10	7 8 9	3jca	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) → ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ∧ 𝐴 ∈ No ) )
11		noreceuw	⊢ ( ( ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ∧ 𝐴 ∈ No ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ∃! 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 )
12	10 11	sylan	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ∃! 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 )
13		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐶 ·s 𝑦 ) = ( 𝐶 ·s 𝐵 ) )
14	13	eqeq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐶 ·s 𝑦 ) = 𝐴 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )
15	14	riota2	⊢ ( ( 𝐵 ∈ No ∧ ∃! 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) → ( ( 𝐶 ·s 𝐵 ) = 𝐴 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
16	6 12 15	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐶 ·s 𝐵 ) = 𝐴 ↔ ( ℩ 𝑦 ∈ No ( 𝐶 ·s 𝑦 ) = 𝐴 ) = 𝐵 ) )
17	5 16	bitr4d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( 𝐶 ∈ No ∧ 𝐶 ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 𝐶 ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 𝐶 ) = 𝐵 ↔ ( 𝐶 ·s 𝐵 ) = 𝐴 ) )