Metamath Proof Explorer

Definition df-suppos

Description: Define the function that, when given an n -ary operation f and n many m -ary operations ( g(/) ) , ..., ( gU. n ) , returns the superposition of f with the ( gi ) , itself another m -ary operation on a . Given x (a sequence of m arguments in a ), the superposition effectively applies each of the ( gi ) to x , then applies f to the resulting sequence of n function values. This can be seen as a generalized version of function composition; see paragraph 3 of Szendrei p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025)

Ref Expression
Assertion df-suppos 
|- suppos = ( a e. _V |-> ( n e. ( _om \ 1o ) , m e. ( _om \ 1o ) |-> ( f e. ( a ^m ( a ^m n ) ) , g e. ( ( a ^m ( a ^m m ) ) ^m n ) |-> ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csuppos 
 |-  suppos
1 va 
 |-  a
2 cvv 
 |-  _V
3 vn 
 |-  n
4 com 
 |-  _om
5 c1o 
 |-  1o
6 4 5 cdif 
 |-  ( _om \ 1o )
7 vm 
 |-  m
8 vf 
 |-  f
9 1 cv 
 |-  a
10 cmap 
 |-  ^m
11 3 cv 
 |-  n
12 9 11 10 co 
 |-  ( a ^m n )
13 9 12 10 co 
 |-  ( a ^m ( a ^m n ) )
14 vg 
 |-  g
15 7 cv 
 |-  m
16 9 15 10 co 
 |-  ( a ^m m )
17 9 16 10 co 
 |-  ( a ^m ( a ^m m ) )
18 17 11 10 co 
 |-  ( ( a ^m ( a ^m m ) ) ^m n )
19 vx 
 |-  x
20 8 cv 
 |-  f
21 vi 
 |-  i
22 14 cv 
 |-  g
23 21 cv 
 |-  i
24 23 22 cfv 
 |-  ( g ` i )
25 19 cv 
 |-  x
26 25 24 cfv 
 |-  ( ( g ` i ) ` x )
27 21 11 26 cmpt 
 |-  ( i e. n |-> ( ( g ` i ) ` x ) )
28 27 20 cfv 
 |-  ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) )
29 19 16 28 cmpt 
 |-  ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) )
30 8 14 13 18 29 cmpo 
 |-  ( f e. ( a ^m ( a ^m n ) ) , g e. ( ( a ^m ( a ^m m ) ) ^m n ) |-> ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) ) )
31 3 7 6 6 30 cmpo 
 |-  ( n e. ( _om \ 1o ) , m e. ( _om \ 1o ) |-> ( f e. ( a ^m ( a ^m n ) ) , g e. ( ( a ^m ( a ^m m ) ) ^m n ) |-> ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) ) ) )
32 1 2 31 cmpt 
 |-  ( a e. _V |-> ( n e. ( _om \ 1o ) , m e. ( _om \ 1o ) |-> ( f e. ( a ^m ( a ^m n ) ) , g e. ( ( a ^m ( a ^m m ) ) ^m n ) |-> ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) ) ) ) )
33 0 32 wceq 
 |-  suppos = ( a e. _V |-> ( n e. ( _om \ 1o ) , m e. ( _om \ 1o ) |-> ( f e. ( a ^m ( a ^m n ) ) , g e. ( ( a ^m ( a ^m m ) ) ^m n ) |-> ( x e. ( a ^m m ) |-> ( f ` ( i e. n |-> ( ( g ` i ) ` x ) ) ) ) ) ) )