Metamath Proof Explorer

Theorem mulsunif

Description: Surreal multiplication has the uniformity property. That is, any cuts that define A and B can be used in the definition of ( A x.s B ) . Theorem 3.5 of Gonshor p. 18. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses mulsunif.1 ⊢ φ → L ≪ s R
mulsunif.2 ⊢ φ → M ≪ s S
mulsunif.3 ⊢ φ → A = L | s R
mulsunif.4 ⊢ φ → B = M | s S
Assertion mulsunif ⊢ φ → A ⋅ s B = a | ∃ p ∈ L ∃ q ∈ M a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ∃ s ∈ S b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ∃ u ∈ S c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ∃ w ∈ M d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 mulsunif.1 ⊢ φ → L ≪ s R
2 mulsunif.2 ⊢ φ → M ≪ s S
3 mulsunif.3 ⊢ φ → A = L | s R
4 mulsunif.4 ⊢ φ → B = M | s S
5 1 2 3 4 mulsuniflem ⊢ φ → A ⋅ s B = e | ∃ f ∈ L ∃ g ∈ M e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ∃ j ∈ S h = i ⋅ s B + s A ⋅ s j - s i ⋅ s j | s k | ∃ l ∈ L ∃ m ∈ S k = l ⋅ s B + s A ⋅ s m - s l ⋅ s m ∪ n | ∃ o ∈ R ∃ x ∈ M n = o ⋅ s B + s A ⋅ s x - s o ⋅ s x
6 mulsval2lem ⊢ a | ∃ p ∈ L ∃ q ∈ M a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q = e | ∃ f ∈ L ∃ g ∈ M e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g
7 mulsval2lem ⊢ b | ∃ r ∈ R ∃ s ∈ S b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s = h | ∃ i ∈ R ∃ j ∈ S h = i ⋅ s B + s A ⋅ s j - s i ⋅ s j
8 6 7 uneq12i ⊢ a | ∃ p ∈ L ∃ q ∈ M a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ∃ s ∈ S b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s = e | ∃ f ∈ L ∃ g ∈ M e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ∃ j ∈ S h = i ⋅ s B + s A ⋅ s j - s i ⋅ s j
9 mulsval2lem ⊢ c | ∃ t ∈ L ∃ u ∈ S c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u = k | ∃ l ∈ L ∃ m ∈ S k = l ⋅ s B + s A ⋅ s m - s l ⋅ s m
10 mulsval2lem ⊢ d | ∃ v ∈ R ∃ w ∈ M d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = n | ∃ o ∈ R ∃ x ∈ M n = o ⋅ s B + s A ⋅ s x - s o ⋅ s x
11 9 10 uneq12i ⊢ c | ∃ t ∈ L ∃ u ∈ S c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ∃ w ∈ M d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = k | ∃ l ∈ L ∃ m ∈ S k = l ⋅ s B + s A ⋅ s m - s l ⋅ s m ∪ n | ∃ o ∈ R ∃ x ∈ M n = o ⋅ s B + s A ⋅ s x - s o ⋅ s x
12 8 11 oveq12i ⊢ a | ∃ p ∈ L ∃ q ∈ M a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ∃ s ∈ S b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ∃ u ∈ S c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ∃ w ∈ M d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = e | ∃ f ∈ L ∃ g ∈ M e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ∃ j ∈ S h = i ⋅ s B + s A ⋅ s j - s i ⋅ s j | s k | ∃ l ∈ L ∃ m ∈ S k = l ⋅ s B + s A ⋅ s m - s l ⋅ s m ∪ n | ∃ o ∈ R ∃ x ∈ M n = o ⋅ s B + s A ⋅ s x - s o ⋅ s x
13 5 12 eqtr4di ⊢ φ → A ⋅ s B = a | ∃ p ∈ L ∃ q ∈ M a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ∃ s ∈ S b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ∃ u ∈ S c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ∃ w ∈ M d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w