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 ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , m ∈ ω ∖ 1 𝑜 ⟼ f ∈ a a n , g ∈ a a m n ⟼ x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 csuppos class suppos
1 va setvar a
2 cvv class V
3 vn setvar n
4 com class ω
5 c1o class 1 𝑜
6 4 5 cdif class ω ∖ 1 𝑜
7 vm setvar m
8 vf setvar f
9 1 cv setvar a
10 cmap class ↑ 𝑚
11 3 cv setvar n
12 9 11 10 co class a n
13 9 12 10 co class a a n
14 vg setvar g
15 7 cv setvar m
16 9 15 10 co class a m
17 9 16 10 co class a a m
18 17 11 10 co class a a m n
19 vx setvar x
20 8 cv setvar f
21 vi setvar i
22 14 cv setvar g
23 21 cv setvar i
24 23 22 cfv class g ⁡ i
25 19 cv setvar x
26 25 24 cfv class g ⁡ i ⁡ x
27 21 11 26 cmpt class i ∈ n ⟼ g ⁡ i ⁡ x
28 27 20 cfv class f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x
29 19 16 28 cmpt class x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x
30 8 14 13 18 29 cmpo class f ∈ a a n , g ∈ a a m n ⟼ x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x
31 3 7 6 6 30 cmpo class n ∈ ω ∖ 1 𝑜 , m ∈ ω ∖ 1 𝑜 ⟼ f ∈ a a n , g ∈ a a m n ⟼ x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x
32 1 2 31 cmpt class a ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , m ∈ ω ∖ 1 𝑜 ⟼ f ∈ a a n , g ∈ a a m n ⟼ x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x
33 0 32 wceq wff suppos = a ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , m ∈ ω ∖ 1 𝑜 ⟼ f ∈ a a n , g ∈ a a m n ⟼ x ∈ a m ⟼ f ⁡ i ∈ n ⟼ g ⁡ i ⁡ x