Metamath Proof Explorer

Theorem muls01

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

Ref Expression
Assertion muls01 
|- ( A e. No -> ( A x.s 0s ) = 0s )

Proof

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