Metamath Proof Explorer

Theorem mulsval2

Description: The value of surreal multiplication, expressed with fewer distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Assertion mulsval2 ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 mulsval ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = e | ∃ f ∈ L ⁡ A ∃ g ∈ L ⁡ B e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ⁡ A ∃ k ∈ R ⁡ B h = i ⋅ s B + s A ⋅ s k - s i ⋅ s k | s l | ∃ m ∈ L ⁡ A ∃ n ∈ R ⁡ B l = m ⋅ s B + s A ⋅ s n - s m ⋅ s n ∪ o | ∃ x ∈ R ⁡ A ∃ y ∈ L ⁡ B o = x ⋅ s B + s A ⋅ s y - s x ⋅ s y
2 mulsval2lem ⊢ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q = e | ∃ f ∈ L ⁡ A ∃ g ∈ L ⁡ B e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g
3 mulsval2lem ⊢ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s = h | ∃ i ∈ R ⁡ A ∃ k ∈ R ⁡ B h = i ⋅ s B + s A ⋅ s k - s i ⋅ s k
4 2 3 uneq12i ⊢ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s = e | ∃ f ∈ L ⁡ A ∃ g ∈ L ⁡ B e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ⁡ A ∃ k ∈ R ⁡ B h = i ⋅ s B + s A ⋅ s k - s i ⋅ s k
5 mulsval2lem ⊢ c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u = l | ∃ m ∈ L ⁡ A ∃ n ∈ R ⁡ B l = m ⋅ s B + s A ⋅ s n - s m ⋅ s n
6 mulsval2lem ⊢ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = o | ∃ x ∈ R ⁡ A ∃ y ∈ L ⁡ B o = x ⋅ s B + s A ⋅ s y - s x ⋅ s y
7 5 6 uneq12i ⊢ c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = l | ∃ m ∈ L ⁡ A ∃ n ∈ R ⁡ B l = m ⋅ s B + s A ⋅ s n - s m ⋅ s n ∪ o | ∃ x ∈ R ⁡ A ∃ y ∈ L ⁡ B o = x ⋅ s B + s A ⋅ s y - s x ⋅ s y
8 4 7 oveq12i ⊢ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w = e | ∃ f ∈ L ⁡ A ∃ g ∈ L ⁡ B e = f ⋅ s B + s A ⋅ s g - s f ⋅ s g ∪ h | ∃ i ∈ R ⁡ A ∃ k ∈ R ⁡ B h = i ⋅ s B + s A ⋅ s k - s i ⋅ s k | s l | ∃ m ∈ L ⁡ A ∃ n ∈ R ⁡ B l = m ⋅ s B + s A ⋅ s n - s m ⋅ s n ∪ o | ∃ x ∈ R ⁡ A ∃ y ∈ L ⁡ B o = x ⋅ s B + s A ⋅ s y - s x ⋅ s y
9 1 8 eqtr4di ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w