Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-opfn Unicode version

Definition df-opfn 25699
Description: Multiplication or addition of two functions  x and  y derived from the operation  g on the elements of the common range of 
x and  y. The functions  x and  y must also have the same domain  i. (Contributed by FL, 15-Oct-2012.)
Assertion
Ref Expression
df-opfn  |-  opfn  =  ( g  e.  _V ,  i  e.  _V  |->  ( x  e.  ( dom  dom  g  ^m  i
) ,  y  e.  ( dom  dom  g  ^m  i )  |->  ( a  e.  dom  x  |->  ( ( x `  a
) g ( y `
 a ) ) ) ) )
Distinct variable group:    g, i, x, y, a

Detailed syntax breakdown of Definition df-opfn
StepHypRef Expression
1 copfn 25698 . 2  class  opfn
2 vg . . 3  set  g
3 vi . . 3  set  i
4 cvv 2801 . . 3  class  _V
5 vx . . . 4  set  x
6 vy . . . 4  set  y
72cv 1631 . . . . . . 7  class  g
87cdm 4705 . . . . . 6  class  dom  g
98cdm 4705 . . . . 5  class  dom  dom  g
103cv 1631 . . . . 5  class  i
11 cmap 6788 . . . . 5  class  ^m
129, 10, 11co 5874 . . . 4  class  ( dom 
dom  g  ^m  i
)
13 va . . . . 5  set  a
145cv 1631 . . . . . 6  class  x
1514cdm 4705 . . . . 5  class  dom  x
1613cv 1631 . . . . . . 7  class  a
1716, 14cfv 5271 . . . . . 6  class  ( x `
 a )
186cv 1631 . . . . . . 7  class  y
1916, 18cfv 5271 . . . . . 6  class  ( y `
 a )
2017, 19, 7co 5874 . . . . 5  class  ( ( x `  a ) g ( y `  a ) )
2113, 15, 20cmpt 4093 . . . 4  class  ( a  e.  dom  x  |->  ( ( x `  a
) g ( y `
 a ) ) )
225, 6, 12, 12, 21cmpt2 5876 . . 3  class  ( x  e.  ( dom  dom  g  ^m  i ) ,  y  e.  ( dom 
dom  g  ^m  i
)  |->  ( a  e. 
dom  x  |->  ( ( x `  a ) g ( y `  a ) ) ) )
232, 3, 4, 4, 22cmpt2 5876 . 2  class  ( g  e.  _V ,  i  e.  _V  |->  ( x  e.  ( dom  dom  g  ^m  i ) ,  y  e.  ( dom 
dom  g  ^m  i
)  |->  ( a  e. 
dom  x  |->  ( ( x `  a ) g ( y `  a ) ) ) ) )
241, 23wceq 1632 1  wff  opfn  =  ( g  e.  _V ,  i  e.  _V  |->  ( x  e.  ( dom  dom  g  ^m  i
) ,  y  e.  ( dom  dom  g  ^m  i )  |->  ( a  e.  dom  x  |->  ( ( x `  a
) g ( y `
 a ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator