This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i1fmullem

Description: Decompose the preimage of a product. (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 i1fmullem 
|- ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( `' ( F oF x. G ) " { A } ) = U_ y e. ( ran G \ { 0 } ) ( ( `' 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 x. G ) Fn RR )
13 12 adantr 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( F oF x. G ) Fn RR )
14 fniniseg 
 |-  ( ( F oF x. G ) Fn RR -> ( z e. ( `' ( F oF x. G ) " { A } ) <-> ( z e. RR /\ ( ( F oF x. G ) ` z ) = A ) ) )
15 13 14 syl 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( `' ( F oF x. G ) " { A } ) <-> ( z e. RR /\ ( ( F oF x. G ) ` z ) = A ) ) )
16 5 adantr 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> F Fn RR )
17 8 adantr 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> G Fn RR )
18 9 a1i 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> RR e. _V )
19 eqidd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ z e. RR ) -> ( F ` z ) = ( F ` z ) )
20 eqidd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ z e. RR ) -> ( G ` z ) = ( G ` z ) )
21 16 17 18 18 11 19 20 ofval 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ z e. RR ) -> ( ( F oF x. G ) ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
22 21 eqeq1d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ z e. RR ) -> ( ( ( F oF x. G ) ` z ) = A <-> ( ( F ` z ) x. ( G ` z ) ) = A ) )
23 22 pm5.32da 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( ( z e. RR /\ ( ( F oF x. G ) ` z ) = A ) <-> ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) )
24 8 ad2antrr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> G Fn RR )
25 simprl 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> z e. RR )
26 fnfvelrn 
 |-  ( ( G Fn RR /\ z e. RR ) -> ( G ` z ) e. ran G )
27 24 25 26 syl2anc 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) e. ran G )
28 eldifsni 
 |-  ( A e. ( CC \ { 0 } ) -> A =/= 0 )
29 28 ad2antlr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> A =/= 0 )
30 simprr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( ( F ` z ) x. ( G ` z ) ) = A )
31 4 ad2antrr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> F : RR --> RR )
32 31 25 ffvelcdmd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( F ` z ) e. RR )
33 32 recnd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( F ` z ) e. CC )
34 33 mul01d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( ( F ` z ) x. 0 ) = 0 )
35 29 30 34 3netr4d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( ( F ` z ) x. ( G ` z ) ) =/= ( ( F ` z ) x. 0 ) )
36 oveq2 
 |-  ( ( G ` z ) = 0 -> ( ( F ` z ) x. ( G ` z ) ) = ( ( F ` z ) x. 0 ) )
37 36 necon3i 
 |-  ( ( ( F ` z ) x. ( G ` z ) ) =/= ( ( F ` z ) x. 0 ) -> ( G ` z ) =/= 0 )
38 35 37 syl 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) =/= 0 )
39 eldifsn 
 |-  ( ( G ` z ) e. ( ran G \ { 0 } ) <-> ( ( G ` z ) e. ran G /\ ( G ` z ) =/= 0 ) )
40 27 38 39 sylanbrc 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) e. ( ran G \ { 0 } ) )
41 7 ad2antrr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> G : RR --> RR )
42 41 25 ffvelcdmd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) e. RR )
43 42 recnd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) e. CC )
44 33 43 38 divcan4d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( ( ( F ` z ) x. ( G ` z ) ) / ( G ` z ) ) = ( F ` z ) )
45 30 oveq1d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( ( ( F ` z ) x. ( G ` z ) ) / ( G ` z ) ) = ( A / ( G ` z ) ) )
46 44 45 eqtr3d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( F ` z ) = ( A / ( G ` z ) ) )
47 31 ffnd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> F Fn RR )
48 fniniseg 
 |-  ( F Fn RR -> ( z e. ( `' F " { ( A / ( G ` z ) ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A / ( G ` z ) ) ) ) )
49 47 48 syl 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( z e. ( `' F " { ( A / ( G ` z ) ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A / ( G ` z ) ) ) ) )
50 25 46 49 mpbir2and 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> z e. ( `' F " { ( A / ( G ` z ) ) } ) )
51 eqidd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( G ` z ) = ( G ` z ) )
52 fniniseg 
 |-  ( G Fn RR -> ( z e. ( `' G " { ( G ` z ) } ) <-> ( z e. RR /\ ( G ` z ) = ( G ` z ) ) ) )
53 24 52 syl 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> ( z e. ( `' G " { ( G ` z ) } ) <-> ( z e. RR /\ ( G ` z ) = ( G ` z ) ) ) )
54 25 51 53 mpbir2and 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> z e. ( `' G " { ( G ` z ) } ) )
55 50 54 elind 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> z e. ( ( `' F " { ( A / ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) )
56 oveq2 
 |-  ( y = ( G ` z ) -> ( A / y ) = ( A / ( G ` z ) ) )
57 56 sneqd 
 |-  ( y = ( G ` z ) -> { ( A / y ) } = { ( A / ( G ` z ) ) } )
58 57 imaeq2d 
 |-  ( y = ( G ` z ) -> ( `' F " { ( A / y ) } ) = ( `' F " { ( A / ( G ` z ) ) } ) )
59 sneq 
 |-  ( y = ( G ` z ) -> { y } = { ( G ` z ) } )
60 59 imaeq2d 
 |-  ( y = ( G ` z ) -> ( `' G " { y } ) = ( `' G " { ( G ` z ) } ) )
61 58 60 ineq12d 
 |-  ( y = ( G ` z ) -> ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) = ( ( `' F " { ( A / ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) )
62 61 eleq2d 
 |-  ( y = ( G ` z ) -> ( z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) <-> z e. ( ( `' F " { ( A / ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) ) )
63 62 rspcev 
 |-  ( ( ( G ` z ) e. ( ran G \ { 0 } ) /\ z e. ( ( `' F " { ( A / ( G ` z ) ) } ) i^i ( `' G " { ( G ` z ) } ) ) ) -> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) )
64 40 55 63 syl2anc 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) -> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) )
65 64 ex 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) -> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) ) )
66 fniniseg 
 |-  ( F Fn RR -> ( z e. ( `' F " { ( A / y ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A / y ) ) ) )
67 16 66 syl 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( `' F " { ( A / y ) } ) <-> ( z e. RR /\ ( F ` z ) = ( A / y ) ) ) )
68 fniniseg 
 |-  ( G Fn RR -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
69 17 68 syl 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
70 67 69 anbi12d 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( ( z e. ( `' F " { ( A / y ) } ) /\ z e. ( `' G " { y } ) ) <-> ( ( z e. RR /\ ( F ` z ) = ( A / y ) ) /\ ( z e. RR /\ ( G ` z ) = y ) ) ) )
71 elin 
 |-  ( z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) <-> ( z e. ( `' F " { ( A / y ) } ) /\ z e. ( `' G " { y } ) ) )
72 anandi 
 |-  ( ( z e. RR /\ ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) ) <-> ( ( z e. RR /\ ( F ` z ) = ( A / y ) ) /\ ( z e. RR /\ ( G ` z ) = y ) ) )
73 70 71 72 3bitr4g 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) <-> ( z e. RR /\ ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) ) ) )
74 73 adantr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) <-> ( z e. RR /\ ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) ) ) )
75 eldifi 
 |-  ( A e. ( CC \ { 0 } ) -> A e. CC )
76 75 ad2antlr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> A e. CC )
77 7 ad2antrr 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> G : RR --> RR )
78 77 frnd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> ran G C_ RR )
79 simprl 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> y e. ( ran G \ { 0 } ) )
80 eldifsn 
 |-  ( y e. ( ran G \ { 0 } ) <-> ( y e. ran G /\ y =/= 0 ) )
81 79 80 sylib 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> ( y e. ran G /\ y =/= 0 ) )
82 81 simpld 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> y e. ran G )
83 78 82 sseldd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> y e. RR )
84 83 recnd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> y e. CC )
85 81 simprd 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> y =/= 0 )
86 76 84 85 divcan1d 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> ( ( A / y ) x. y ) = A )
87 oveq12 
 |-  ( ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) -> ( ( F ` z ) x. ( G ` z ) ) = ( ( A / y ) x. y ) )
88 87 eqeq1d 
 |-  ( ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) -> ( ( ( F ` z ) x. ( G ` z ) ) = A <-> ( ( A / y ) x. y ) = A ) )
89 86 88 syl5ibrcom 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ ( y e. ( ran G \ { 0 } ) /\ z e. RR ) ) -> ( ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) -> ( ( F ` z ) x. ( G ` z ) ) = A ) )
90 89 anassrs 
 |-  ( ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) -> ( ( F ` z ) x. ( G ` z ) ) = A ) )
91 90 imdistanda 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ y e. ( ran G \ { 0 } ) ) -> ( ( z e. RR /\ ( ( F ` z ) = ( A / y ) /\ ( G ` z ) = y ) ) -> ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) )
92 74 91 sylbid 
 |-  ( ( ( ph /\ A e. ( CC \ { 0 } ) ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) -> ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) )
93 92 rexlimdva 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) -> ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) ) )
94 65 93 impbid 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( ( z e. RR /\ ( ( F ` z ) x. ( G ` z ) ) = A ) <-> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) ) )
95 15 23 94 3bitrd 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( `' ( F oF x. G ) " { A } ) <-> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) ) )
96 eliun 
 |-  ( z e. U_ y e. ( ran G \ { 0 } ) ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) <-> E. y e. ( ran G \ { 0 } ) z e. ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) )
97 95 96 bitr4di 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( z e. ( `' ( F oF x. G ) " { A } ) <-> z e. U_ y e. ( ran G \ { 0 } ) ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) ) )
98 97 eqrdv 
 |-  ( ( ph /\ A e. ( CC \ { 0 } ) ) -> ( `' ( F oF x. G ) " { A } ) = U_ y e. ( ran G \ { 0 } ) ( ( `' F " { ( A / y ) } ) i^i ( `' G " { y } ) ) )