Metamath Proof Explorer

Theorem xrge0iifhom

Description: The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
xrge0iifhmeo.k 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
Assertion xrge0iifhom 
|- ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 xrge0iifhmeo.k 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3 0xr 
 |-  0 e. RR*
4 1xr 
 |-  1 e. RR*
5 0le1 
 |-  0 <_ 1
6 snunioc 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ 0 <_ 1 ) -> ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 ) )
7 3 4 5 6 mp3an 
 |-  ( { 0 } u. ( 0 (,] 1 ) ) = ( 0 [,] 1 )
8 7 eleq2i 
 |-  ( Y e. ( { 0 } u. ( 0 (,] 1 ) ) <-> Y e. ( 0 [,] 1 ) )
9 elun 
 |-  ( Y e. ( { 0 } u. ( 0 (,] 1 ) ) <-> ( Y e. { 0 } \/ Y e. ( 0 (,] 1 ) ) )
10 8 9 bitr3i 
 |-  ( Y e. ( 0 [,] 1 ) <-> ( Y e. { 0 } \/ Y e. ( 0 (,] 1 ) ) )
11 elsni 
 |-  ( Y e. { 0 } -> Y = 0 )
12 11 orim1i 
 |-  ( ( Y e. { 0 } \/ Y e. ( 0 (,] 1 ) ) -> ( Y = 0 \/ Y e. ( 0 (,] 1 ) ) )
13 10 12 sylbi 
 |-  ( Y e. ( 0 [,] 1 ) -> ( Y = 0 \/ Y e. ( 0 (,] 1 ) ) )
14 0elunit 
 |-  0 e. ( 0 [,] 1 )
15 iftrue 
 |-  ( x = 0 -> if ( x = 0 , +oo , -u ( log ` x ) ) = +oo )
16 pnfex 
 |-  +oo e. _V
17 15 1 16 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( F ` 0 ) = +oo )
18 14 17 ax-mp 
 |-  ( F ` 0 ) = +oo
19 18 oveq2i 
 |-  ( ( F ` X ) +e ( F ` 0 ) ) = ( ( F ` X ) +e +oo )
20 eqeq1 
 |-  ( x = X -> ( x = 0 <-> X = 0 ) )
21 fveq2 
 |-  ( x = X -> ( log ` x ) = ( log ` X ) )
22 21 negeqd 
 |-  ( x = X -> -u ( log ` x ) = -u ( log ` X ) )
23 20 22 ifbieq2d 
 |-  ( x = X -> if ( x = 0 , +oo , -u ( log ` x ) ) = if ( X = 0 , +oo , -u ( log ` X ) ) )
24 negex 
 |-  -u ( log ` X ) e. _V
25 16 24 ifex 
 |-  if ( X = 0 , +oo , -u ( log ` X ) ) e. _V
26 23 1 25 fvmpt 
 |-  ( X e. ( 0 [,] 1 ) -> ( F ` X ) = if ( X = 0 , +oo , -u ( log ` X ) ) )
27 pnfxr 
 |-  +oo e. RR*
28 27 a1i 
 |-  ( ( X e. ( 0 [,] 1 ) /\ X = 0 ) -> +oo e. RR* )
29 elunitrn 
 |-  ( X e. ( 0 [,] 1 ) -> X e. RR )
30 29 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> X e. RR )
31 elunitge0 
 |-  ( X e. ( 0 [,] 1 ) -> 0 <_ X )
32 31 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> 0 <_ X )
33 simpr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> -. X = 0 )
34 33 neqned 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> X =/= 0 )
35 30 32 34 ne0gt0d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> 0 < X )
36 30 35 elrpd 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> X e. RR+ )
37 36 relogcld 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> ( log ` X ) e. RR )
38 37 renegcld 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> -u ( log ` X ) e. RR )
39 38 rexrd 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> -u ( log ` X ) e. RR* )
40 28 39 ifclda 
 |-  ( X e. ( 0 [,] 1 ) -> if ( X = 0 , +oo , -u ( log ` X ) ) e. RR* )
41 26 40 eqeltrd 
 |-  ( X e. ( 0 [,] 1 ) -> ( F ` X ) e. RR* )
42 41 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` X ) e. RR* )
43 neeq1 
 |-  ( +oo = if ( X = 0 , +oo , -u ( log ` X ) ) -> ( +oo =/= -oo <-> if ( X = 0 , +oo , -u ( log ` X ) ) =/= -oo ) )
44 neeq1 
 |-  ( -u ( log ` X ) = if ( X = 0 , +oo , -u ( log ` X ) ) -> ( -u ( log ` X ) =/= -oo <-> if ( X = 0 , +oo , -u ( log ` X ) ) =/= -oo ) )
45 pnfnemnf 
 |-  +oo =/= -oo
46 45 a1i 
 |-  ( ( X e. ( 0 [,] 1 ) /\ X = 0 ) -> +oo =/= -oo )
47 38 renemnfd 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X = 0 ) -> -u ( log ` X ) =/= -oo )
48 43 44 46 47 ifbothda 
 |-  ( X e. ( 0 [,] 1 ) -> if ( X = 0 , +oo , -u ( log ` X ) ) =/= -oo )
49 26 48 eqnetrd 
 |-  ( X e. ( 0 [,] 1 ) -> ( F ` X ) =/= -oo )
50 49 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` X ) =/= -oo )
51 xaddpnf1 
 |-  ( ( ( F ` X ) e. RR* /\ ( F ` X ) =/= -oo ) -> ( ( F ` X ) +e +oo ) = +oo )
52 42 50 51 syl2anc 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( ( F ` X ) +e +oo ) = +oo )
53 19 52 eqtrid 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( ( F ` X ) +e ( F ` 0 ) ) = +oo )
54 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
55 simpl 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> X e. ( 0 [,] 1 ) )
56 54 55 sselid 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> X e. CC )
57 56 mul01d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( X x. 0 ) = 0 )
58 57 fveq2d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` ( X x. 0 ) ) = ( F ` 0 ) )
59 58 18 eqtrdi 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` ( X x. 0 ) ) = +oo )
60 53 59 eqtr4d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( ( F ` X ) +e ( F ` 0 ) ) = ( F ` ( X x. 0 ) ) )
61 simpr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> Y = 0 )
62 61 fveq2d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` Y ) = ( F ` 0 ) )
63 62 oveq2d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( ( F ` X ) +e ( F ` Y ) ) = ( ( F ` X ) +e ( F ` 0 ) ) )
64 61 oveq2d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( X x. Y ) = ( X x. 0 ) )
65 64 fveq2d 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` ( X x. Y ) ) = ( F ` ( X x. 0 ) ) )
66 60 63 65 3eqtr4rd 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y = 0 ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
67 7 eleq2i 
 |-  ( X e. ( { 0 } u. ( 0 (,] 1 ) ) <-> X e. ( 0 [,] 1 ) )
68 elun 
 |-  ( X e. ( { 0 } u. ( 0 (,] 1 ) ) <-> ( X e. { 0 } \/ X e. ( 0 (,] 1 ) ) )
69 67 68 bitr3i 
 |-  ( X e. ( 0 [,] 1 ) <-> ( X e. { 0 } \/ X e. ( 0 (,] 1 ) ) )
70 elsni 
 |-  ( X e. { 0 } -> X = 0 )
71 70 orim1i 
 |-  ( ( X e. { 0 } \/ X e. ( 0 (,] 1 ) ) -> ( X = 0 \/ X e. ( 0 (,] 1 ) ) )
72 69 71 sylbi 
 |-  ( X e. ( 0 [,] 1 ) -> ( X = 0 \/ X e. ( 0 (,] 1 ) ) )
73 18 oveq1i 
 |-  ( ( F ` 0 ) +e ( F ` Y ) ) = ( +oo +e ( F ` Y ) )
74 simpr 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> Y e. ( 0 (,] 1 ) )
75 1 xrge0iifcv 
 |-  ( Y e. ( 0 (,] 1 ) -> ( F ` Y ) = -u ( log ` Y ) )
76 0le0 
 |-  0 <_ 0
77 1re 
 |-  1 e. RR
78 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
79 77 78 ax-mp 
 |-  1 < +oo
80 iocssioo 
 |-  ( ( ( 0 e. RR* /\ +oo e. RR* ) /\ ( 0 <_ 0 /\ 1 < +oo ) ) -> ( 0 (,] 1 ) C_ ( 0 (,) +oo ) )
81 3 27 76 79 80 mp4an 
 |-  ( 0 (,] 1 ) C_ ( 0 (,) +oo )
82 ioorp 
 |-  ( 0 (,) +oo ) = RR+
83 81 82 sseqtri 
 |-  ( 0 (,] 1 ) C_ RR+
84 83 sseli 
 |-  ( Y e. ( 0 (,] 1 ) -> Y e. RR+ )
85 84 relogcld 
 |-  ( Y e. ( 0 (,] 1 ) -> ( log ` Y ) e. RR )
86 85 renegcld 
 |-  ( Y e. ( 0 (,] 1 ) -> -u ( log ` Y ) e. RR )
87 75 86 eqeltrd 
 |-  ( Y e. ( 0 (,] 1 ) -> ( F ` Y ) e. RR )
88 87 rexrd 
 |-  ( Y e. ( 0 (,] 1 ) -> ( F ` Y ) e. RR* )
89 74 88 syl 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` Y ) e. RR* )
90 87 renemnfd 
 |-  ( Y e. ( 0 (,] 1 ) -> ( F ` Y ) =/= -oo )
91 74 90 syl 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` Y ) =/= -oo )
92 xaddpnf2 
 |-  ( ( ( F ` Y ) e. RR* /\ ( F ` Y ) =/= -oo ) -> ( +oo +e ( F ` Y ) ) = +oo )
93 89 91 92 syl2anc 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( +oo +e ( F ` Y ) ) = +oo )
94 73 93 eqtrid 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( ( F ` 0 ) +e ( F ` Y ) ) = +oo )
95 rpssre 
 |-  RR+ C_ RR
96 83 95 sstri 
 |-  ( 0 (,] 1 ) C_ RR
97 ax-resscn 
 |-  RR C_ CC
98 96 97 sstri 
 |-  ( 0 (,] 1 ) C_ CC
99 98 74 sselid 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> Y e. CC )
100 99 mul02d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( 0 x. Y ) = 0 )
101 100 fveq2d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( 0 x. Y ) ) = ( F ` 0 ) )
102 101 18 eqtrdi 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( 0 x. Y ) ) = +oo )
103 94 102 eqtr4d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( ( F ` 0 ) +e ( F ` Y ) ) = ( F ` ( 0 x. Y ) ) )
104 simpl 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> X = 0 )
105 104 fveq2d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` X ) = ( F ` 0 ) )
106 105 oveq1d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( ( F ` X ) +e ( F ` Y ) ) = ( ( F ` 0 ) +e ( F ` Y ) ) )
107 104 fvoveq1d 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( F ` ( 0 x. Y ) ) )
108 103 106 107 3eqtr4rd 
 |-  ( ( X = 0 /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
109 simpl 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> X e. ( 0 (,] 1 ) )
110 83 109 sselid 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> X e. RR+ )
111 110 relogcld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( log ` X ) e. RR )
112 111 renegcld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> -u ( log ` X ) e. RR )
113 simpr 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> Y e. ( 0 (,] 1 ) )
114 83 113 sselid 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> Y e. RR+ )
115 114 relogcld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( log ` Y ) e. RR )
116 115 renegcld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> -u ( log ` Y ) e. RR )
117 rexadd 
 |-  ( ( -u ( log ` X ) e. RR /\ -u ( log ` Y ) e. RR ) -> ( -u ( log ` X ) +e -u ( log ` Y ) ) = ( -u ( log ` X ) + -u ( log ` Y ) ) )
118 112 116 117 syl2anc 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( -u ( log ` X ) +e -u ( log ` Y ) ) = ( -u ( log ` X ) + -u ( log ` Y ) ) )
119 1 xrge0iifcv 
 |-  ( X e. ( 0 (,] 1 ) -> ( F ` X ) = -u ( log ` X ) )
120 119 75 oveqan12d 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( ( F ` X ) +e ( F ` Y ) ) = ( -u ( log ` X ) +e -u ( log ` Y ) ) )
121 110 rpred 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> X e. RR )
122 114 rpred 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> Y e. RR )
123 121 122 remulcld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( X x. Y ) e. RR )
124 110 rpgt0d 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> 0 < X )
125 114 rpgt0d 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> 0 < Y )
126 121 122 124 125 mulgt0d 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> 0 < ( X x. Y ) )
127 iocssicc 
 |-  ( 0 (,] 1 ) C_ ( 0 [,] 1 )
128 127 109 sselid 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> X e. ( 0 [,] 1 ) )
129 127 113 sselid 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> Y e. ( 0 [,] 1 ) )
130 iimulcl 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> ( X x. Y ) e. ( 0 [,] 1 ) )
131 128 129 130 syl2anc 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( X x. Y ) e. ( 0 [,] 1 ) )
132 elicc01 
 |-  ( ( X x. Y ) e. ( 0 [,] 1 ) <-> ( ( X x. Y ) e. RR /\ 0 <_ ( X x. Y ) /\ ( X x. Y ) <_ 1 ) )
133 132 simp3bi 
 |-  ( ( X x. Y ) e. ( 0 [,] 1 ) -> ( X x. Y ) <_ 1 )
134 131 133 syl 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( X x. Y ) <_ 1 )
135 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( ( X x. Y ) e. ( 0 (,] 1 ) <-> ( ( X x. Y ) e. RR /\ 0 < ( X x. Y ) /\ ( X x. Y ) <_ 1 ) ) )
136 3 77 135 mp2an 
 |-  ( ( X x. Y ) e. ( 0 (,] 1 ) <-> ( ( X x. Y ) e. RR /\ 0 < ( X x. Y ) /\ ( X x. Y ) <_ 1 ) )
137 123 126 134 136 syl3anbrc 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( X x. Y ) e. ( 0 (,] 1 ) )
138 1 xrge0iifcv 
 |-  ( ( X x. Y ) e. ( 0 (,] 1 ) -> ( F ` ( X x. Y ) ) = -u ( log ` ( X x. Y ) ) )
139 137 138 syl 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = -u ( log ` ( X x. Y ) ) )
140 110 114 relogmuld 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( log ` ( X x. Y ) ) = ( ( log ` X ) + ( log ` Y ) ) )
141 140 negeqd 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> -u ( log ` ( X x. Y ) ) = -u ( ( log ` X ) + ( log ` Y ) ) )
142 111 recnd 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( log ` X ) e. CC )
143 115 recnd 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( log ` Y ) e. CC )
144 142 143 negdid 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> -u ( ( log ` X ) + ( log ` Y ) ) = ( -u ( log ` X ) + -u ( log ` Y ) ) )
145 139 141 144 3eqtrd 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( -u ( log ` X ) + -u ( log ` Y ) ) )
146 118 120 145 3eqtr4rd 
 |-  ( ( X e. ( 0 (,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
147 108 146 jaoian 
 |-  ( ( ( X = 0 \/ X e. ( 0 (,] 1 ) ) /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
148 72 147 sylan 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 (,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
149 66 148 jaodan 
 |-  ( ( X e. ( 0 [,] 1 ) /\ ( Y = 0 \/ Y e. ( 0 (,] 1 ) ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )
150 13 149 sylan2 
 |-  ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> ( F ` ( X x. Y ) ) = ( ( F ` X ) +e ( F ` Y ) ) )