Metamath Proof Explorer

Theorem mulsproplem10

Description: Lemma for surreal multiplication. State the cut properties of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 ⊢ φ → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
mulsproplem9.1 ⊢ φ → A ∈ No
mulsproplem9.2 ⊢ φ → B ∈ No
Assertion mulsproplem10 ⊢ φ → A ⋅ s B ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 mulsproplem.1 ⊢ φ → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
2 mulsproplem9.1 ⊢ φ → A ∈ No
3 mulsproplem9.2 ⊢ φ → B ∈ No
4 1 2 3 mulsproplem9 ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
5 scutcut ⊢ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
6 4 5 syl ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
7 mulsval ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B = g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
8 2 3 7 syl2anc ⊢ φ → A ⋅ s B = g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
9 8 eleq1d ⊢ φ → A ⋅ s B ∈ No ↔ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No
10 8 sneqd ⊢ φ → A ⋅ s B = g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
11 10 breq2d ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ↔ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
12 10 breq1d ⊢ φ → A ⋅ s B ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
13 9 11 12 3anbi123d ⊢ φ → A ⋅ s B ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s | s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
14 6 13 mpbird ⊢ φ → A ⋅ s B ∈ No ∧ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w