Metamath Proof Explorer


Theorem mulscut

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

Ref Expression
Hypotheses mulscut.1 φ A No
mulscut.2 φ B No
Assertion mulscut φ 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 mulscut.1 φ A No
2 mulscut.2 φ B No
3 1 2 mulscutlem φ 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