Metamath Proof Explorer

Theorem i1faddlem

Description: Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses i1fadd.1 
|- ( ph -> F e. dom S.1 )
i1fadd.2 
|- ( ph -> G e. dom S.1 )
Assertion i1faddlem 
|- ( ( ph /\ A e. CC ) -> ( `' ( F oF + G ) " { A } ) = U_ y e. ran G ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )

Proof

Step Hyp Ref Expression
1 i1fadd.1 
 |-  ( ph -> F e. dom S.1 )
2 i1fadd.2 
 |-  ( ph -> G e. dom S.1 )
3 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
4 1 3 syl 
 |-  ( ph -> F : RR --> RR )
5 4 ffnd 
 |-  ( ph -> F Fn RR )
6 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
7 2 6 syl 
 |-  ( ph -> G : RR --> RR )
8 7 ffnd 
 |-  ( ph -> G Fn RR )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 inidm 
 |-  ( RR i^i RR ) = RR
12 5 8 10 10 11 offn 
 |-  ( ph -> ( F oF + G ) Fn RR )
13 12 adantr 
 |-  ( ( ph /\ A e. CC ) -> ( F oF + G ) Fn RR )
14 fniniseg 
 |-  ( ( F oF + G ) Fn RR -> ( z e. ( `' ( F oF + G ) " { A } ) <-> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
15 13 14 syl 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( `' ( F oF + G ) " { A } ) <-> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
16 8 ad2antrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> G Fn RR )
17 simprl 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> z e. RR )
18 fnfvelrn 
 |-  ( ( G Fn RR /\ z e. RR ) -> ( G ` z ) e. ran G )
19 16 17 18 syl2anc 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( G ` z ) e. ran G )
20 simprr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( ( F oF + G ) ` z ) = A )
21 eqidd 
 |-  ( ( ph /\ z e. RR ) -> ( F ` z ) = ( F ` z ) )
22 eqidd 
 |-  ( ( ph /\ z e. RR ) -> ( G ` z ) = ( G ` z ) )
23 5 8 10 10 11 21 22 ofval 
 |-  ( ( ph /\ z e. RR ) -> ( ( F oF + G ) ` z ) = ( ( F ` z ) + ( G ` z ) ) )
24 23 ad2ant2r 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( ( F oF + G ) ` z ) = ( ( F ` z ) + ( G ` z ) ) )
25 20 24 eqtr3d 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> A = ( ( F ` z ) + ( G ` z ) ) )
26 25 oveq1d 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( A - ( G ` z ) ) = ( ( ( F ` z ) + ( G ` z ) ) - ( G ` z ) ) )
27 ax-resscn 
 |-  RR C_ CC
28 fss 
 |-  ( ( F : RR --> RR /\ RR C_ CC ) -> F : RR --> CC )
29 4 27 28 sylancl 
 |-  ( ph -> F : RR --> CC )
30 29 ad2antrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> F : RR --> CC )
31 30 17 ffvelrnd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( F ` z ) e. CC )
32 fss 
 |-  ( ( G : RR --> RR /\ RR C_ CC ) -> G : RR --> CC )
33 7 27 32 sylancl 
 |-  ( ph -> G : RR --> CC )
34 33 ad2antrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> G : RR --> CC )
35 34 17 ffvelrnd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( G ` z ) e. CC )
36 31 35 pncand 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( ( ( F ` z ) + ( G ` z ) ) - ( G ` z ) ) = ( F ` z ) )
37 26 36 eqtr2d 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( F ` z ) = ( A - ( G ` z ) ) )
38 5 ad2antrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> F Fn RR )
39 fniniseg 
 |-  ( F Fn RR -> ( z e. ( `' F " { ( A - ( G ` z ) ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A - ( G ` z ) ) ) ) )
40 38 39 syl 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( z e. ( `' F " { ( A - ( G ` z ) ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A - ( G ` z ) ) ) ) )
41 17 37 40 mpbir2and 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> z e. ( `' F " { ( A - ( G ` z ) ) } ) )
42 eqidd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( G ` z ) = ( G ` z ) )
43 fniniseg 
 |-  ( G Fn RR -> ( z e. ( `' G " { ( G ` z ) } ) <-> ( z e. RR /\ ( G ` z ) = ( G ` z ) ) ) )
44 16 43 syl 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> ( z e. ( `' G " { ( G ` z ) } ) <-> ( z e. RR /\ ( G ` z ) = ( G ` z ) ) ) )
45 17 42 44 mpbir2and 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> z e. ( `' G " { ( G ` z ) } ) )
46 41 45 elind 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> z e. ( ( `' F " { ( A - ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) )
47 oveq2 
 |-  ( y = ( G ` z ) -> ( A - y ) = ( A - ( G ` z ) ) )
48 47 sneqd 
 |-  ( y = ( G ` z ) -> { ( A - y ) } = { ( A - ( G ` z ) ) } )
49 48 imaeq2d 
 |-  ( y = ( G ` z ) -> ( `' F " { ( A - y ) } ) = ( `' F " { ( A - ( G ` z ) ) } ) )
50 sneq 
 |-  ( y = ( G ` z ) -> { y } = { ( G ` z ) } )
51 50 imaeq2d 
 |-  ( y = ( G ` z ) -> ( `' G " { y } ) = ( `' G " { ( G ` z ) } ) )
52 49 51 ineq12d 
 |-  ( y = ( G ` z ) -> ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) = ( ( `' F " { ( A - ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) )
53 52 eleq2d 
 |-  ( y = ( G ` z ) -> ( z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) <-> z e. ( ( `' F " { ( A - ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) ) )
54 53 rspcev 
 |-  ( ( ( G ` z ) e. ran G /\ z e. ( ( `' F " { ( A - ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) ) -> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )
55 19 46 54 syl2anc 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) -> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )
56 55 ex 
 |-  ( ( ph /\ A e. CC ) -> ( ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) -> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) ) )
57 elin 
 |-  ( z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) <-> ( z e. ( `' F " { ( A - y ) } ) /\ z e. ( `' G " { y } ) ) )
58 5 adantr 
 |-  ( ( ph /\ A e. CC ) -> F Fn RR )
59 fniniseg 
 |-  ( F Fn RR -> ( z e. ( `' F " { ( A - y ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A - y ) ) ) )
60 58 59 syl 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( `' F " { ( A - y ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A - y ) ) ) )
61 8 adantr 
 |-  ( ( ph /\ A e. CC ) -> G Fn RR )
62 fniniseg 
 |-  ( G Fn RR -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
63 61 62 syl 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
64 60 63 anbi12d 
 |-  ( ( ph /\ A e. CC ) -> ( ( z e. ( `' F " { ( A - y ) } ) /\ z e. ( `' G " { y } ) ) <-> ( ( z e. RR /\ ( F ` z ) = ( A - y ) ) /\ ( z e. RR /\ ( G ` z ) = y ) ) ) )
65 anandi 
 |-  ( ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) <-> ( ( z e. RR /\ ( F ` z ) = ( A - y ) ) /\ ( z e. RR /\ ( G ` z ) = y ) ) )
66 simprl 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> z e. RR )
67 23 ad2ant2r 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( ( F oF + G ) ` z ) = ( ( F ` z ) + ( G ` z ) ) )
68 simprrl 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( F ` z ) = ( A - y ) )
69 simprrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( G ` z ) = y )
70 68 69 oveq12d 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( ( F ` z ) + ( G ` z ) ) = ( ( A - y ) + y ) )
71 simplr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> A e. CC )
72 33 ad2antrr 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> G : RR --> CC )
73 72 66 ffvelrnd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( G ` z ) e. CC )
74 69 73 eqeltrrd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> y e. CC )
75 71 74 npcand 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( ( A - y ) + y ) = A )
76 67 70 75 3eqtrd 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( ( F oF + G ) ` z ) = A )
77 66 76 jca 
 |-  ( ( ( ph /\ A e. CC ) /\ ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) )
78 77 ex 
 |-  ( ( ph /\ A e. CC ) -> ( ( z e. RR /\ ( ( F ` z ) = ( A - y ) /\ ( G ` z ) = y ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
79 65 78 syl5bir 
 |-  ( ( ph /\ A e. CC ) -> ( ( ( z e. RR /\ ( F ` z ) = ( A - y ) ) /\ ( z e. RR /\ ( G ` z ) = y ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
80 64 79 sylbid 
 |-  ( ( ph /\ A e. CC ) -> ( ( z e. ( `' F " { ( A - y ) } ) /\ z e. ( `' G " { y } ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
81 57 80 syl5bi 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
82 81 rexlimdvw 
 |-  ( ( ph /\ A e. CC ) -> ( E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) -> ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) ) )
83 56 82 impbid 
 |-  ( ( ph /\ A e. CC ) -> ( ( z e. RR /\ ( ( F oF + G ) ` z ) = A ) <-> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) ) )
84 15 83 bitrd 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( `' ( F oF + G ) " { A } ) <-> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) ) )
85 eliun 
 |-  ( z e. U_ y e. ran G ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) <-> E. y e. ran G z e. ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )
86 84 85 bitr4di 
 |-  ( ( ph /\ A e. CC ) -> ( z e. ( `' ( F oF + G ) " { A } ) <-> z e. U_ y e. ran G ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) ) )
87 86 eqrdv 
 |-  ( ( ph /\ A e. CC ) -> ( `' ( F oF + G ) " { A } ) = U_ y e. ran G ( ( `' F " { ( A - y ) } ) i^i ( `' G " { y } ) ) )