Metamath Proof Explorer

Theorem divmulsw

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 divmuls ). (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divmulsw ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → A / su C = B ↔ C ⋅ s B = A

Proof

Step Hyp Ref Expression
1 divsval ⊢ A ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = ι y ∈ No | C ⋅ s y = A
2 1 eqeq1d ⊢ A ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = B ↔ ι y ∈ No | C ⋅ s y = A = B
3 2 3expb ⊢ A ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = B ↔ ι y ∈ No | C ⋅ s y = A = B
4 3 3adant2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A / su C = B ↔ ι y ∈ No | C ⋅ s y = A = B
5 4 adantr ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → A / su C = B ↔ ι y ∈ No | C ⋅ s y = A = B
6 simpl2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → B ∈ No
7 simp3l ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → C ∈ No
8 simp3r ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → C ≠ 0 s
9 simp1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → A ∈ No
10 7 8 9 3jca ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s → C ∈ No ∧ C ≠ 0 s ∧ A ∈ No
11 noreceuw ⊢ C ∈ No ∧ C ≠ 0 s ∧ A ∈ No ∧ ∃ x ∈ No C ⋅ s x = 1 s → ∃! y ∈ No C ⋅ s y = A
12 10 11 sylan ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → ∃! y ∈ No C ⋅ s y = A
13 oveq2 ⊢ y = B → C ⋅ s y = C ⋅ s B
14 13 eqeq1d ⊢ y = B → C ⋅ s y = A ↔ C ⋅ s B = A
15 14 riota2 ⊢ B ∈ No ∧ ∃! y ∈ No C ⋅ s y = A → C ⋅ s B = A ↔ ι y ∈ No | C ⋅ s y = A = B
16 6 12 15 syl2anc ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → C ⋅ s B = A ↔ ι y ∈ No | C ⋅ s y = A = B
17 5 16 bitr4d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ C ≠ 0 s ∧ ∃ x ∈ No C ⋅ s x = 1 s → A / su C = B ↔ C ⋅ s B = A