Metamath Proof Explorer


Theorem muls01

Description: Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion muls01 A No A s 0 s = 0 s

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 mulsval A No 0 s No A s 0 s = a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s | s c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w
3 1 2 mpan2 A No A s 0 s = a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s | s c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w
4 rex0 ¬ q a = p s 0 s + s A s q - s p s q
5 left0s L 0 s =
6 5 rexeqi q L 0 s a = p s 0 s + s A s q - s p s q q a = p s 0 s + s A s q - s p s q
7 4 6 mtbir ¬ q L 0 s a = p s 0 s + s A s q - s p s q
8 7 a1i p L A ¬ q L 0 s a = p s 0 s + s A s q - s p s q
9 8 nrex ¬ p L A q L 0 s a = p s 0 s + s A s q - s p s q
10 9 abf a | p L A q L 0 s a = p s 0 s + s A s q - s p s q =
11 rex0 ¬ s b = r s 0 s + s A s s - s r s s
12 right0s R 0 s =
13 12 rexeqi s R 0 s b = r s 0 s + s A s s - s r s s s b = r s 0 s + s A s s - s r s s
14 11 13 mtbir ¬ s R 0 s b = r s 0 s + s A s s - s r s s
15 14 a1i r R A ¬ s R 0 s b = r s 0 s + s A s s - s r s s
16 15 nrex ¬ r R A s R 0 s b = r s 0 s + s A s s - s r s s
17 16 abf b | r R A s R 0 s b = r s 0 s + s A s s - s r s s =
18 10 17 uneq12i a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s =
19 un0 =
20 18 19 eqtri a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s =
21 rex0 ¬ u c = t s 0 s + s A s u - s t s u
22 12 rexeqi u R 0 s c = t s 0 s + s A s u - s t s u u c = t s 0 s + s A s u - s t s u
23 21 22 mtbir ¬ u R 0 s c = t s 0 s + s A s u - s t s u
24 23 a1i t L A ¬ u R 0 s c = t s 0 s + s A s u - s t s u
25 24 nrex ¬ t L A u R 0 s c = t s 0 s + s A s u - s t s u
26 25 abf c | t L A u R 0 s c = t s 0 s + s A s u - s t s u =
27 rex0 ¬ w d = v s 0 s + s A s w - s v s w
28 5 rexeqi w L 0 s d = v s 0 s + s A s w - s v s w w d = v s 0 s + s A s w - s v s w
29 27 28 mtbir ¬ w L 0 s d = v s 0 s + s A s w - s v s w
30 29 a1i v R A ¬ w L 0 s d = v s 0 s + s A s w - s v s w
31 30 nrex ¬ v R A w L 0 s d = v s 0 s + s A s w - s v s w
32 31 abf d | v R A w L 0 s d = v s 0 s + s A s w - s v s w =
33 26 32 uneq12i c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w =
34 33 19 eqtri c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w =
35 20 34 oveq12i a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s | s c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w = | s
36 df-0s 0 s = | s
37 35 36 eqtr4i a | p L A q L 0 s a = p s 0 s + s A s q - s p s q b | r R A s R 0 s b = r s 0 s + s A s s - s r s s | s c | t L A u R 0 s c = t s 0 s + s A s u - s t s u d | v R A w L 0 s d = v s 0 s + s A s w - s v s w = 0 s
38 3 37 eqtrdi A No A s 0 s = 0 s