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 ⊢ φ → L ≪ s R
mulsunif2.2 ⊢ φ → M ≪ s S
mulsunif2.3 ⊢ φ → A = L | s R
mulsunif2.4 ⊢ φ → B = M | s S
Assertion mulsunif2 Could not format assertion : No typesetting found for |- ( 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 ) ) ) } ) ) ) with typecode |-

Proof

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