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 ffvelrnda
 |-  ( ( ( ( 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 syl5bb
 |-  ( ( ( ( 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 ) } ) )