Metamath Proof Explorer

Theorem mulcut2

Description: Show that the cut involved in surreal multiplication is actually a cut. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses mulcut.1 ⊢ φ → A ∈ No
mulcut.2 ⊢ φ → B ∈ No
Assertion mulcut2 ⊢ φ → 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 mulcut.1 ⊢ φ → A ∈ No
2 mulcut.2 ⊢ φ → B ∈ No
3 1 2 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
4 3anass ⊢ 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 ∧ 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
5 3 4 sylib ⊢ φ → 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
6 5 simprd ⊢ φ → 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
7 ovex ⊢ A ⋅ s B ∈ V
8 7 snnz ⊢ A ⋅ s B ≠ ∅
9 sltstr ⊢ 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 ≠ ∅ → 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
10 8 9 mp3an3 ⊢ 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 | ∃ 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
11 6 10 syl ⊢ φ → 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