Metamath Proof Explorer

Theorem divsval

Description: The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divsval ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B = ι x ∈ No | B ⋅ s x = A

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ B ∈ No ∖ 0 s ↔ B ∈ No ∧ B ≠ 0 s
2 eqeq2 ⊢ y = A → z ⋅ s x = y ↔ z ⋅ s x = A
3 2 riotabidv ⊢ y = A → ι x ∈ No | z ⋅ s x = y = ι x ∈ No | z ⋅ s x = A
4 oveq1 ⊢ z = B → z ⋅ s x = B ⋅ s x
5 4 eqeq1d ⊢ z = B → z ⋅ s x = A ↔ B ⋅ s x = A
6 5 riotabidv ⊢ z = B → ι x ∈ No | z ⋅ s x = A = ι x ∈ No | B ⋅ s x = A
7 df-divs ⊢ / su = y ∈ No , z ∈ No ∖ 0 s ⟼ ι x ∈ No | z ⋅ s x = y
8 riotaex ⊢ ι x ∈ No | B ⋅ s x = A ∈ V
9 3 6 7 8 ovmpo ⊢ A ∈ No ∧ B ∈ No ∖ 0 s → A / su B = ι x ∈ No | B ⋅ s x = A
10 1 9 sylan2br ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B = ι x ∈ No | B ⋅ s x = A
11 10 3impb ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B = ι x ∈ No | B ⋅ s x = A