Metamath Proof Explorer

Theorem i1fmulc

Description: A nonnegative constant times a simple function gives another simple 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 i1fmulc 
|- ( ph -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )

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 /\ A = 0 ) -> RR e. _V )
5 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
6 1 5 syl 
 |-  ( ph -> F : RR --> RR )
7 6 adantr 
 |-  ( ( ph /\ A = 0 ) -> F : RR --> RR )
8 2 adantr 
 |-  ( ( ph /\ A = 0 ) -> A e. RR )
9 0red 
 |-  ( ( ph /\ A = 0 ) -> 0 e. RR )
10 simplr 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> A = 0 )
11 10 oveq1d 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( A x. x ) = ( 0 x. x ) )
12 mul02lem2 
 |-  ( x e. RR -> ( 0 x. x ) = 0 )
13 12 adantl 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( 0 x. x ) = 0 )
14 11 13 eqtrd 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( A x. x ) = 0 )
15 4 7 8 9 14 caofid2 
 |-  ( ( ph /\ A = 0 ) -> ( ( RR X. { A } ) oF x. F ) = ( RR X. { 0 } ) )
16 i1f0 
 |-  ( RR X. { 0 } ) e. dom S.1
17 15 16 eqeltrdi 
 |-  ( ( ph /\ A = 0 ) -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )
18 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
19 18 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
20 fconst6g 
 |-  ( A e. RR -> ( RR X. { A } ) : RR --> RR )
21 2 20 syl 
 |-  ( ph -> ( RR X. { A } ) : RR --> RR )
22 3 a1i 
 |-  ( ph -> RR e. _V )
23 inidm 
 |-  ( RR i^i RR ) = RR
24 19 21 6 22 22 23 off 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
25 24 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
26 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
27 1 26 syl 
 |-  ( ph -> ran F e. Fin )
28 ovex 
 |-  ( A x. y ) e. _V
29 eqid 
 |-  ( y e. ran F |-> ( A x. y ) ) = ( y e. ran F |-> ( A x. y ) )
30 28 29 fnmpti 
 |-  ( y e. ran F |-> ( A x. y ) ) Fn ran F
31 dffn4 
 |-  ( ( y e. ran F |-> ( A x. y ) ) Fn ran F <-> ( y e. ran F |-> ( A x. y ) ) : ran F -onto-> ran ( y e. ran F |-> ( A x. y ) ) )
32 30 31 mpbi 
 |-  ( y e. ran F |-> ( A x. y ) ) : ran F -onto-> ran ( y e. ran F |-> ( A x. y ) )
33 fofi 
 |-  ( ( ran F e. Fin /\ ( y e. ran F |-> ( A x. y ) ) : ran F -onto-> ran ( y e. ran F |-> ( A x. y ) ) ) -> ran ( y e. ran F |-> ( A x. y ) ) e. Fin )
34 27 32 33 sylancl 
 |-  ( ph -> ran ( y e. ran F |-> ( A x. y ) ) e. Fin )
35 id 
 |-  ( w e. ran F -> w e. ran F )
36 elsni 
 |-  ( x e. { A } -> x = A )
37 36 oveq1d 
 |-  ( x e. { A } -> ( x x. w ) = ( A x. w ) )
38 oveq2 
 |-  ( y = w -> ( A x. y ) = ( A x. w ) )
39 38 rspceeqv 
 |-  ( ( w e. ran F /\ ( x x. w ) = ( A x. w ) ) -> E. y e. ran F ( x x. w ) = ( A x. y ) )
40 35 37 39 syl2anr 
 |-  ( ( x e. { A } /\ w e. ran F ) -> E. y e. ran F ( x x. w ) = ( A x. y ) )
41 ovex 
 |-  ( x x. w ) e. _V
42 eqeq1 
 |-  ( z = ( x x. w ) -> ( z = ( A x. y ) <-> ( x x. w ) = ( A x. y ) ) )
43 42 rexbidv 
 |-  ( z = ( x x. w ) -> ( E. y e. ran F z = ( A x. y ) <-> E. y e. ran F ( x x. w ) = ( A x. y ) ) )
44 41 43 elab 
 |-  ( ( x x. w ) e. { z | E. y e. ran F z = ( A x. y ) } <-> E. y e. ran F ( x x. w ) = ( A x. y ) )
45 40 44 sylibr 
 |-  ( ( x e. { A } /\ w e. ran F ) -> ( x x. w ) e. { z | E. y e. ran F z = ( A x. y ) } )
46 45 adantl 
 |-  ( ( ph /\ ( x e. { A } /\ w e. ran F ) ) -> ( x x. w ) e. { z | E. y e. ran F z = ( A x. y ) } )
47 fconstg 
 |-  ( A e. RR -> ( RR X. { A } ) : RR --> { A } )
48 2 47 syl 
 |-  ( ph -> ( RR X. { A } ) : RR --> { A } )
49 6 ffnd 
 |-  ( ph -> F Fn RR )
50 dffn3 
 |-  ( F Fn RR <-> F : RR --> ran F )
51 49 50 sylib 
 |-  ( ph -> F : RR --> ran F )
52 46 48 51 22 22 23 off 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) : RR --> { z | E. y e. ran F z = ( A x. y ) } )
53 52 frnd 
 |-  ( ph -> ran ( ( RR X. { A } ) oF x. F ) C_ { z | E. y e. ran F z = ( A x. y ) } )
54 29 rnmpt 
 |-  ran ( y e. ran F |-> ( A x. y ) ) = { z | E. y e. ran F z = ( A x. y ) }
55 53 54 sseqtrrdi 
 |-  ( ph -> ran ( ( RR X. { A } ) oF x. F ) C_ ran ( y e. ran F |-> ( A x. y ) ) )
56 34 55 ssfid 
 |-  ( ph -> ran ( ( RR X. { A } ) oF x. F ) e. Fin )
57 56 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ran ( ( RR X. { A } ) oF x. F ) e. Fin )
58 24 frnd 
 |-  ( ph -> ran ( ( RR X. { A } ) oF x. F ) C_ RR )
59 58 ssdifssd 
 |-  ( ph -> ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ RR )
60 59 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ RR )
61 60 sselda 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> y e. RR )
62 1 2 i1fmulclem 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { y } ) = ( `' F " { ( y / A ) } ) )
63 61 62 syldan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { y } ) = ( `' F " { ( y / A ) } ) )
64 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { ( y / A ) } ) e. dom vol )
65 1 64 syl 
 |-  ( ph -> ( `' F " { ( y / A ) } ) e. dom vol )
66 65 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( `' F " { ( y / A ) } ) e. dom vol )
67 63 66 eqeltrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { y } ) e. dom vol )
68 63 fveq2d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { y } ) ) = ( vol ` ( `' F " { ( y / A ) } ) ) )
69 1 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> F e. dom S.1 )
70 2 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. RR )
71 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A =/= 0 )
72 61 70 71 redivcld 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( y / A ) e. RR )
73 61 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> y e. CC )
74 70 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. CC )
75 eldifsni 
 |-  ( y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -> y =/= 0 )
76 75 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> y =/= 0 )
77 73 74 76 71 divne0d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( y / A ) =/= 0 )
78 eldifsn 
 |-  ( ( y / A ) e. ( RR \ { 0 } ) <-> ( ( y / A ) e. RR /\ ( y / A ) =/= 0 ) )
79 72 77 78 sylanbrc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( y / A ) e. ( RR \ { 0 } ) )
80 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ ( y / A ) e. ( RR \ { 0 } ) ) -> ( vol ` ( `' F " { ( y / A ) } ) ) e. RR )
81 69 79 80 syl2anc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' F " { ( y / A ) } ) ) e. RR )
82 68 81 eqeltrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { y } ) ) e. RR )
83 25 57 67 82 i1fd 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )
84 17 83 pm2.61dane 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )