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 and derived from the operation on the elements of the common range of and . The functions and must also have the same domain . (Contributed by FL, 15-Oct-2012.)
Assertion
Ref Expression
df-opfn
Distinct variable group:   ,,,,

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