Metamath Proof Explorer

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 𝐵 ) = 𝐴 ) )