Metamath Proof Explorer

Theorem mulsunif2

Description: Alternate expression for surreal multiplication. Note from Conway p. 19. (Contributed by Scott Fenton, 16-Mar-2025)

Ref Expression
Hypotheses mulsunif2.1 
|- ( ph -> L <
mulsunif2.2 
|- ( ph -> M <
mulsunif2.3 
|- ( ph -> A = ( L |s R ) )
mulsunif2.4 
|- ( ph -> B = ( M |s S ) )
Assertion mulsunif2 
|- ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) } u. { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 mulsunif2.1 
 |-  ( ph -> L <
2 mulsunif2.2 
 |-  ( ph -> M <
3 mulsunif2.3 
 |-  ( ph -> A = ( L |s R ) )
4 mulsunif2.4 
 |-  ( ph -> B = ( M |s S ) )
5 1 2 3 4 mulsunif2lem 
 |-  ( ph -> ( A x.s B ) = ( ( { e | E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) } u. { f | E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) } ) |s ( { g | E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) } u. { h | E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) } ) ) )
6 eqeq1 
 |-  ( e = a -> ( e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) <-> a = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) ) )
7 6 2rexbidv 
 |-  ( e = a -> ( E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) <-> E. i e. L E. j e. M a = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) ) )
8 oveq2 
 |-  ( i = p -> ( A -s i ) = ( A -s p ) )
9 8 oveq1d 
 |-  ( i = p -> ( ( A -s i ) x.s ( B -s j ) ) = ( ( A -s p ) x.s ( B -s j ) ) )
10 9 oveq2d 
 |-  ( i = p -> ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s j ) ) ) )
11 10 eqeq2d 
 |-  ( i = p -> ( a = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) <-> a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s j ) ) ) ) )
12 oveq2 
 |-  ( j = q -> ( B -s j ) = ( B -s q ) )
13 12 oveq2d 
 |-  ( j = q -> ( ( A -s p ) x.s ( B -s j ) ) = ( ( A -s p ) x.s ( B -s q ) ) )
14 13 oveq2d 
 |-  ( j = q -> ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s j ) ) ) = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) )
15 14 eqeq2d 
 |-  ( j = q -> ( a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s j ) ) ) <-> a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) ) )
16 11 15 cbvrex2vw 
 |-  ( E. i e. L E. j e. M a = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) <-> E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) )
17 7 16 bitrdi 
 |-  ( e = a -> ( E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) <-> E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) ) )
18 17 cbvabv 
 |-  { e | E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) } = { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) }
19 eqeq1 
 |-  ( f = b -> ( f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) <-> b = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) ) )
20 19 2rexbidv 
 |-  ( f = b -> ( E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) <-> E. k e. R E. l e. S b = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) ) )
21 oveq1 
 |-  ( k = r -> ( k -s A ) = ( r -s A ) )
22 21 oveq1d 
 |-  ( k = r -> ( ( k -s A ) x.s ( l -s B ) ) = ( ( r -s A ) x.s ( l -s B ) ) )
23 22 oveq2d 
 |-  ( k = r -> ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) = ( ( A x.s B ) -s ( ( r -s A ) x.s ( l -s B ) ) ) )
24 23 eqeq2d 
 |-  ( k = r -> ( b = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) <-> b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( l -s B ) ) ) ) )
25 oveq1 
 |-  ( l = s -> ( l -s B ) = ( s -s B ) )
26 25 oveq2d 
 |-  ( l = s -> ( ( r -s A ) x.s ( l -s B ) ) = ( ( r -s A ) x.s ( s -s B ) ) )
27 26 oveq2d 
 |-  ( l = s -> ( ( A x.s B ) -s ( ( r -s A ) x.s ( l -s B ) ) ) = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) )
28 27 eqeq2d 
 |-  ( l = s -> ( b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( l -s B ) ) ) <-> b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) ) )
29 24 28 cbvrex2vw 
 |-  ( E. k e. R E. l e. S b = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) <-> E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) )
30 20 29 bitrdi 
 |-  ( f = b -> ( E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) <-> E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) ) )
31 30 cbvabv 
 |-  { f | E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) } = { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) }
32 18 31 uneq12i 
 |-  ( { e | E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) } u. { f | E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) } ) = ( { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) } u. { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) } )
33 eqeq1 
 |-  ( g = c -> ( g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) <-> c = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) ) )
34 33 2rexbidv 
 |-  ( g = c -> ( E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) <-> E. m e. L E. n e. S c = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) ) )
35 oveq2 
 |-  ( m = t -> ( A -s m ) = ( A -s t ) )
36 35 oveq1d 
 |-  ( m = t -> ( ( A -s m ) x.s ( n -s B ) ) = ( ( A -s t ) x.s ( n -s B ) ) )
37 36 oveq2d 
 |-  ( m = t -> ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) = ( ( A x.s B ) +s ( ( A -s t ) x.s ( n -s B ) ) ) )
38 37 eqeq2d 
 |-  ( m = t -> ( c = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) <-> c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( n -s B ) ) ) ) )
39 oveq1 
 |-  ( n = u -> ( n -s B ) = ( u -s B ) )
40 39 oveq2d 
 |-  ( n = u -> ( ( A -s t ) x.s ( n -s B ) ) = ( ( A -s t ) x.s ( u -s B ) ) )
41 40 oveq2d 
 |-  ( n = u -> ( ( A x.s B ) +s ( ( A -s t ) x.s ( n -s B ) ) ) = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) )
42 41 eqeq2d 
 |-  ( n = u -> ( c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( n -s B ) ) ) <-> c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
43 38 42 cbvrex2vw 
 |-  ( E. m e. L E. n e. S c = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) <-> E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) )
44 34 43 bitrdi 
 |-  ( g = c -> ( E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) <-> E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) ) )
45 44 cbvabv 
 |-  { g | E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) } = { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) }
46 eqeq1 
 |-  ( h = d -> ( h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) <-> d = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) ) )
47 46 2rexbidv 
 |-  ( h = d -> ( E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) <-> E. o e. R E. x e. M d = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) ) )
48 oveq1 
 |-  ( o = v -> ( o -s A ) = ( v -s A ) )
49 48 oveq1d 
 |-  ( o = v -> ( ( o -s A ) x.s ( B -s x ) ) = ( ( v -s A ) x.s ( B -s x ) ) )
50 49 oveq2d 
 |-  ( o = v -> ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s x ) ) ) )
51 50 eqeq2d 
 |-  ( o = v -> ( d = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) <-> d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s x ) ) ) ) )
52 oveq2 
 |-  ( x = w -> ( B -s x ) = ( B -s w ) )
53 52 oveq2d 
 |-  ( x = w -> ( ( v -s A ) x.s ( B -s x ) ) = ( ( v -s A ) x.s ( B -s w ) ) )
54 53 oveq2d 
 |-  ( x = w -> ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s x ) ) ) = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) )
55 54 eqeq2d 
 |-  ( x = w -> ( d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s x ) ) ) <-> d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) ) )
56 51 55 cbvrex2vw 
 |-  ( E. o e. R E. x e. M d = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) <-> E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) )
57 47 56 bitrdi 
 |-  ( h = d -> ( E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) <-> E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) ) )
58 57 cbvabv 
 |-  { h | E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) } = { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) }
59 45 58 uneq12i 
 |-  ( { g | E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) } u. { h | E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) } ) = ( { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) } )
60 32 59 oveq12i 
 |-  ( ( { e | E. i e. L E. j e. M e = ( ( A x.s B ) -s ( ( A -s i ) x.s ( B -s j ) ) ) } u. { f | E. k e. R E. l e. S f = ( ( A x.s B ) -s ( ( k -s A ) x.s ( l -s B ) ) ) } ) |s ( { g | E. m e. L E. n e. S g = ( ( A x.s B ) +s ( ( A -s m ) x.s ( n -s B ) ) ) } u. { h | E. o e. R E. x e. M h = ( ( A x.s B ) +s ( ( o -s A ) x.s ( B -s x ) ) ) } ) ) = ( ( { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) } u. { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) } ) )
61 5 60 eqtrdi 
 |-  ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( A x.s B ) -s ( ( A -s p ) x.s ( B -s q ) ) ) } u. { b | E. r e. R E. s e. S b = ( ( A x.s B ) -s ( ( r -s A ) x.s ( s -s B ) ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( A x.s B ) +s ( ( A -s t ) x.s ( u -s B ) ) ) } u. { d | E. v e. R E. w e. M d = ( ( A x.s B ) +s ( ( v -s A ) x.s ( B -s w ) ) ) } ) ) )