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 25596
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 25595 . 2  class  opfn
2 vg . . 3  set  g
3 vi . . 3  set  i
4 cvv 2788 . . 3  class  _V
5 vx . . . 4  set  x
6 vy . . . 4  set  y
72cv 1622 . . . . . . 7  class  g
87cdm 4689 . . . . . 6  class  dom  g
98cdm 4689 . . . . 5  class  dom  dom  g
103cv 1622 . . . . 5  class  i
11 cmap 6772 . . . . 5  class  ^m
129, 10, 11co 5858 . . . 4  class  ( dom 
dom  g  ^m  i
)
13 va . . . . 5  set  a
145cv 1622 . . . . . 6  class  x
1514cdm 4689 . . . . 5  class  dom  x
1613cv 1622 . . . . . . 7  class  a
1716, 14cfv 5255 . . . . . 6  class  ( x `
 a )
186cv 1622 . . . . . . 7  class  y
1916, 18cfv 5255 . . . . . 6  class  ( y `
 a )
2017, 19, 7co 5858 . . . . 5  class  ( ( x `  a ) g ( y `  a ) )
2113, 15, 20cmpt 4077 . . . 4  class  ( a  e.  dom  x  |->  ( ( x `  a
) g ( y `
 a ) ) )
225, 6, 12, 12, 21cmpt2 5860 . . 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 5860 . 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 1623 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