Metamath Proof Explorer

Theorem i1fmulclem

Description: Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses i1fmulc.2 
|- ( ph -> F e. dom S.1 )
i1fmulc.3 
|- ( ph -> A e. RR )
Assertion i1fmulclem 
|- ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) = ( `' F " { ( B / A ) } ) )

Proof

Step Hyp Ref Expression
1 i1fmulc.2 
 |-  ( ph -> F e. dom S.1 )
2 i1fmulc.3 
 |-  ( ph -> A e. RR )
3 reex 
 |-  RR e. _V
4 3 a1i 
 |-  ( ph -> RR e. _V )
5 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
6 1 5 syl 
 |-  ( ph -> F : RR --> RR )
7 6 ffnd 
 |-  ( ph -> F Fn RR )
8 eqidd 
 |-  ( ( ph /\ z e. RR ) -> ( F ` z ) = ( F ` z ) )
9 4 2 7 8 ofc1 
 |-  ( ( ph /\ z e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` z ) = ( A x. ( F ` z ) ) )
10 9 ad4ant14 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` z ) = ( A x. ( F ` z ) ) )
11 10 eqeq1d 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` z ) = B <-> ( A x. ( F ` z ) ) = B ) )
12 eqcom 
 |-  ( ( F ` z ) = ( B / A ) <-> ( B / A ) = ( F ` z ) )
13 simplr 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> B e. RR )
14 13 recnd 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> B e. CC )
15 2 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A e. RR )
16 15 recnd 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A e. CC )
17 6 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> F : RR --> RR )
18 17 ffvelcdmda 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( F ` z ) e. RR )
19 18 recnd 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( F ` z ) e. CC )
20 simpllr 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> A =/= 0 )
21 14 16 19 20 divmuld 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( B / A ) = ( F ` z ) <-> ( A x. ( F ` z ) ) = B ) )
22 12 21 bitrid 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( F ` z ) = ( B / A ) <-> ( A x. ( F ` z ) ) = B ) )
23 11 22 bitr4d 
 |-  ( ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) /\ z e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` z ) = B <-> ( F ` z ) = ( B / A ) ) )
24 23 pm5.32da 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) )
25 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
26 25 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
27 fconstg 
 |-  ( A e. RR -> ( RR X. { A } ) : RR --> { A } )
28 2 27 syl 
 |-  ( ph -> ( RR X. { A } ) : RR --> { A } )
29 2 snssd 
 |-  ( ph -> { A } C_ RR )
30 28 29 fssd 
 |-  ( ph -> ( RR X. { A } ) : RR --> RR )
31 inidm 
 |-  ( RR i^i RR ) = RR
32 26 30 6 4 4 31 off 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
33 32 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
34 33 ffnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( ( RR X. { A } ) oF x. F ) Fn RR )
35 fniniseg 
 |-  ( ( ( RR X. { A } ) oF x. F ) Fn RR -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) ) )
36 34 35 syl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> ( z e. RR /\ ( ( ( RR X. { A } ) oF x. F ) ` z ) = B ) ) )
37 17 ffnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> F Fn RR )
38 fniniseg 
 |-  ( F Fn RR -> ( z e. ( `' F " { ( B / A ) } ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) )
39 37 38 syl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' F " { ( B / A ) } ) <-> ( z e. RR /\ ( F ` z ) = ( B / A ) ) ) )
40 24 36 39 3bitr4d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( z e. ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) <-> z e. ( `' F " { ( B / A ) } ) ) )
41 40 eqrdv 
 |-  ( ( ( ph /\ A =/= 0 ) /\ B e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { B } ) = ( `' F " { ( B / A ) } ) )