Metamath Proof Explorer

Theorem mulcut

Description: Show the cut properties of surreal multiplication. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses mulcut.1 ⊢ φ → A ∈ No
mulcut.2 ⊢ φ → B ∈ No
Assertion mulcut ⊢ φ → A ⋅ s B ∈ No ∧ 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 A ⋅ s B ∧ A ⋅ s B ≪ 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 mulcut.1 ⊢ φ → A ∈ No
2 mulcut.2 ⊢ φ → B ∈ No
3 1 2 mulcutlem ⊢ φ → A ⋅ s B ∈ No ∧ f | ∃ g ∈ L ⁡ A ∃ h ∈ L ⁡ B f = g ⋅ s B + s A ⋅ s h - s g ⋅ s h ∪ i | ∃ j ∈ R ⁡ A ∃ k ∈ R ⁡ B i = j ⋅ s B + s A ⋅ s k - s j ⋅ s k ≪ s A ⋅ s B ∧ A ⋅ s B ≪ 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
4 biid ⊢ A ⋅ s B ∈ No ↔ A ⋅ s B ∈ No
5 mulsval2lem ⊢ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q = f | ∃ g ∈ L ⁡ A ∃ h ∈ L ⁡ B f = g ⋅ s B + s A ⋅ s h - s g ⋅ s h
6 mulsval2lem ⊢ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s = i | ∃ j ∈ R ⁡ A ∃ k ∈ R ⁡ B i = j ⋅ s B + s A ⋅ s k - s j ⋅ s k
7 5 6 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 = f | ∃ g ∈ L ⁡ A ∃ h ∈ L ⁡ B f = g ⋅ s B + s A ⋅ s h - s g ⋅ s h ∪ i | ∃ j ∈ R ⁡ A ∃ k ∈ R ⁡ B i = j ⋅ s B + s A ⋅ s k - s j ⋅ s k
8 7 breq1i ⊢ 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 A ⋅ s B ↔ f | ∃ g ∈ L ⁡ A ∃ h ∈ L ⁡ B f = g ⋅ s B + s A ⋅ s h - s g ⋅ s h ∪ i | ∃ j ∈ R ⁡ A ∃ k ∈ R ⁡ B i = j ⋅ s B + s A ⋅ s k - s j ⋅ s k ≪ s A ⋅ s B
9 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
10 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
11 9 10 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
12 11 breq2i ⊢ A ⋅ s B ≪ 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 ↔ A ⋅ s B ≪ 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
13 4 8 12 3anbi123i ⊢ A ⋅ s B ∈ No ∧ 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 A ⋅ s B ∧ A ⋅ s B ≪ 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 ↔ A ⋅ s B ∈ No ∧ f | ∃ g ∈ L ⁡ A ∃ h ∈ L ⁡ B f = g ⋅ s B + s A ⋅ s h - s g ⋅ s h ∪ i | ∃ j ∈ R ⁡ A ∃ k ∈ R ⁡ B i = j ⋅ s B + s A ⋅ s k - s j ⋅ s k ≪ s A ⋅ s B ∧ A ⋅ s B ≪ 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
14 3 13 sylibr ⊢ φ → A ⋅ s B ∈ No ∧ 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 A ⋅ s B ∧ A ⋅ s B ≪ 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