Metamath Proof Explorer

Theorem itg1mulc

Description: The integral of a constant times a simple function is the constant times the original integral. (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 itg1mulc 
|- ( ph -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.1 ` F ) ) )

Proof

Step Hyp Ref Expression
1 i1fmulc.2 
 |-  ( ph -> F e. dom S.1 )
2 i1fmulc.3 
 |-  ( ph -> A e. RR )
3 itg10 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = 0
4 reex 
 |-  RR e. _V
5 4 a1i 
 |-  ( ( ph /\ A = 0 ) -> RR e. _V )
6 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
7 1 6 syl 
 |-  ( ph -> F : RR --> RR )
8 7 adantr 
 |-  ( ( ph /\ A = 0 ) -> F : RR --> RR )
9 2 adantr 
 |-  ( ( ph /\ A = 0 ) -> A e. RR )
10 0red 
 |-  ( ( ph /\ A = 0 ) -> 0 e. RR )
11 simplr 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> A = 0 )
12 11 oveq1d 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( A x. x ) = ( 0 x. x ) )
13 mul02lem2 
 |-  ( x e. RR -> ( 0 x. x ) = 0 )
14 13 adantl 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( 0 x. x ) = 0 )
15 12 14 eqtrd 
 |-  ( ( ( ph /\ A = 0 ) /\ x e. RR ) -> ( A x. x ) = 0 )
16 5 8 9 10 15 caofid2 
 |-  ( ( ph /\ A = 0 ) -> ( ( RR X. { A } ) oF x. F ) = ( RR X. { 0 } ) )
17 16 fveq2d 
 |-  ( ( ph /\ A = 0 ) -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( S.1 ` ( RR X. { 0 } ) ) )
18 simpr 
 |-  ( ( ph /\ A = 0 ) -> A = 0 )
19 18 oveq1d 
 |-  ( ( ph /\ A = 0 ) -> ( A x. ( S.1 ` F ) ) = ( 0 x. ( S.1 ` F ) ) )
20 itg1cl 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. RR )
21 1 20 syl 
 |-  ( ph -> ( S.1 ` F ) e. RR )
22 21 recnd 
 |-  ( ph -> ( S.1 ` F ) e. CC )
23 22 mul02d 
 |-  ( ph -> ( 0 x. ( S.1 ` F ) ) = 0 )
24 23 adantr 
 |-  ( ( ph /\ A = 0 ) -> ( 0 x. ( S.1 ` F ) ) = 0 )
25 19 24 eqtrd 
 |-  ( ( ph /\ A = 0 ) -> ( A x. ( S.1 ` F ) ) = 0 )
26 3 17 25 3eqtr4a 
 |-  ( ( ph /\ A = 0 ) -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.1 ` F ) ) )
27 1 2 i1fmulc 
 |-  ( ph -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )
28 27 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( RR X. { A } ) oF x. F ) e. dom S.1 )
29 i1ff 
 |-  ( ( ( RR X. { A } ) oF x. F ) e. dom S.1 -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
30 28 29 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( RR X. { A } ) oF x. F ) : RR --> RR )
31 30 frnd 
 |-  ( ( ph /\ A =/= 0 ) -> ran ( ( RR X. { A } ) oF x. F ) C_ RR )
32 31 ssdifssd 
 |-  ( ( ph /\ A =/= 0 ) -> ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ RR )
33 32 sselda 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> m e. RR )
34 33 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> m e. CC )
35 2 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> A e. RR )
36 35 recnd 
 |-  ( ( ph /\ A =/= 0 ) -> A e. CC )
37 36 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. CC )
38 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A =/= 0 )
39 34 37 38 divcan2d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( A x. ( m / A ) ) = m )
40 1 2 i1fmulclem 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. RR ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) = ( `' F " { ( m / A ) } ) )
41 33 40 syldan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) = ( `' F " { ( m / A ) } ) )
42 41 fveq2d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) = ( vol ` ( `' F " { ( m / A ) } ) ) )
43 42 eqcomd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' F " { ( m / A ) } ) ) = ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) )
44 39 43 oveq12d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( ( A x. ( m / A ) ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) = ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) )
45 2 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. RR )
46 33 45 38 redivcld 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( m / A ) e. RR )
47 46 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( m / A ) e. CC )
48 1 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> F e. dom S.1 )
49 45 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. CC )
50 eldifsni 
 |-  ( m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -> m =/= 0 )
51 50 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> m =/= 0 )
52 34 49 51 38 divne0d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( m / A ) =/= 0 )
53 eldifsn 
 |-  ( ( m / A ) e. ( RR \ { 0 } ) <-> ( ( m / A ) e. RR /\ ( m / A ) =/= 0 ) )
54 46 52 53 sylanbrc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( m / A ) e. ( RR \ { 0 } ) )
55 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ ( m / A ) e. ( RR \ { 0 } ) ) -> ( vol ` ( `' F " { ( m / A ) } ) ) e. RR )
56 48 54 55 syl2anc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' F " { ( m / A ) } ) ) e. RR )
57 56 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( vol ` ( `' F " { ( m / A ) } ) ) e. CC )
58 37 47 57 mulassd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( ( A x. ( m / A ) ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) = ( A x. ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
59 44 58 eqtr3d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) = ( A x. ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
60 59 sumeq2dv 
 |-  ( ( ph /\ A =/= 0 ) -> sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( A x. ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
61 i1frn 
 |-  ( ( ( RR X. { A } ) oF x. F ) e. dom S.1 -> ran ( ( RR X. { A } ) oF x. F ) e. Fin )
62 28 61 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ran ( ( RR X. { A } ) oF x. F ) e. Fin )
63 difss 
 |-  ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ ran ( ( RR X. { A } ) oF x. F )
64 ssfi 
 |-  ( ( ran ( ( RR X. { A } ) oF x. F ) e. Fin /\ ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ ran ( ( RR X. { A } ) oF x. F ) ) -> ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) e. Fin )
65 62 63 64 sylancl 
 |-  ( ( ph /\ A =/= 0 ) -> ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) e. Fin )
66 47 57 mulcld 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) e. CC )
67 65 36 66 fsummulc2 
 |-  ( ( ph /\ A =/= 0 ) -> ( A x. sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( A x. ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
68 60 67 eqtr4d 
 |-  ( ( ph /\ A =/= 0 ) -> sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) = ( A x. sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
69 itg1val 
 |-  ( ( ( RR X. { A } ) oF x. F ) e. dom S.1 -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) )
70 28 69 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( m x. ( vol ` ( `' ( ( RR X. { A } ) oF x. F ) " { m } ) ) ) )
71 1 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> F e. dom S.1 )
72 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
73 71 72 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
74 id 
 |-  ( k = ( m / A ) -> k = ( m / A ) )
75 sneq 
 |-  ( k = ( m / A ) -> { k } = { ( m / A ) } )
76 75 imaeq2d 
 |-  ( k = ( m / A ) -> ( `' F " { k } ) = ( `' F " { ( m / A ) } ) )
77 76 fveq2d 
 |-  ( k = ( m / A ) -> ( vol ` ( `' F " { k } ) ) = ( vol ` ( `' F " { ( m / A ) } ) ) )
78 74 77 oveq12d 
 |-  ( k = ( m / A ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) = ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) )
79 eqid 
 |-  ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) |-> ( n / A ) ) = ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) |-> ( n / A ) )
80 eldifi 
 |-  ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -> n e. ran ( ( RR X. { A } ) oF x. F ) )
81 4 a1i 
 |-  ( ph -> RR e. _V )
82 7 ffnd 
 |-  ( ph -> F Fn RR )
83 eqidd 
 |-  ( ( ph /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
84 81 2 82 83 ofc1 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` y ) = ( A x. ( F ` y ) ) )
85 84 adantlr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` y ) = ( A x. ( F ` y ) ) )
86 85 oveq1d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) = ( ( A x. ( F ` y ) ) / A ) )
87 7 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> F : RR --> RR )
88 87 ffvelcdmda 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( F ` y ) e. RR )
89 88 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( F ` y ) e. CC )
90 36 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> A e. CC )
91 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> A =/= 0 )
92 89 90 91 divcan3d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( A x. ( F ` y ) ) / A ) = ( F ` y ) )
93 86 92 eqtrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) = ( F ` y ) )
94 87 ffnd 
 |-  ( ( ph /\ A =/= 0 ) -> F Fn RR )
95 fnfvelrn 
 |-  ( ( F Fn RR /\ y e. RR ) -> ( F ` y ) e. ran F )
96 94 95 sylan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( F ` y ) e. ran F )
97 93 96 eqeltrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) e. ran F )
98 97 ralrimiva 
 |-  ( ( ph /\ A =/= 0 ) -> A. y e. RR ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) e. ran F )
99 30 ffnd 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( RR X. { A } ) oF x. F ) Fn RR )
100 oveq1 
 |-  ( n = ( ( ( RR X. { A } ) oF x. F ) ` y ) -> ( n / A ) = ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) )
101 100 eleq1d 
 |-  ( n = ( ( ( RR X. { A } ) oF x. F ) ` y ) -> ( ( n / A ) e. ran F <-> ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) e. ran F ) )
102 101 ralrn 
 |-  ( ( ( RR X. { A } ) oF x. F ) Fn RR -> ( A. n e. ran ( ( RR X. { A } ) oF x. F ) ( n / A ) e. ran F <-> A. y e. RR ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) e. ran F ) )
103 99 102 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( A. n e. ran ( ( RR X. { A } ) oF x. F ) ( n / A ) e. ran F <-> A. y e. RR ( ( ( ( RR X. { A } ) oF x. F ) ` y ) / A ) e. ran F ) )
104 98 103 mpbird 
 |-  ( ( ph /\ A =/= 0 ) -> A. n e. ran ( ( RR X. { A } ) oF x. F ) ( n / A ) e. ran F )
105 104 r19.21bi 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ran ( ( RR X. { A } ) oF x. F ) ) -> ( n / A ) e. ran F )
106 80 105 sylan2 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( n / A ) e. ran F )
107 32 sselda 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> n e. RR )
108 107 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> n e. CC )
109 36 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A e. CC )
110 eldifsni 
 |-  ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -> n =/= 0 )
111 110 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> n =/= 0 )
112 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> A =/= 0 )
113 108 109 111 112 divne0d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( n / A ) =/= 0 )
114 eldifsn 
 |-  ( ( n / A ) e. ( ran F \ { 0 } ) <-> ( ( n / A ) e. ran F /\ ( n / A ) =/= 0 ) )
115 106 113 114 sylanbrc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( n / A ) e. ( ran F \ { 0 } ) )
116 eldifi 
 |-  ( k e. ( ran F \ { 0 } ) -> k e. ran F )
117 fnfvelrn 
 |-  ( ( ( ( RR X. { A } ) oF x. F ) Fn RR /\ y e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` y ) e. ran ( ( RR X. { A } ) oF x. F ) )
118 99 117 sylan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( ( ( RR X. { A } ) oF x. F ) ` y ) e. ran ( ( RR X. { A } ) oF x. F ) )
119 85 118 eqeltrrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ y e. RR ) -> ( A x. ( F ` y ) ) e. ran ( ( RR X. { A } ) oF x. F ) )
120 119 ralrimiva 
 |-  ( ( ph /\ A =/= 0 ) -> A. y e. RR ( A x. ( F ` y ) ) e. ran ( ( RR X. { A } ) oF x. F ) )
121 oveq2 
 |-  ( k = ( F ` y ) -> ( A x. k ) = ( A x. ( F ` y ) ) )
122 121 eleq1d 
 |-  ( k = ( F ` y ) -> ( ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) <-> ( A x. ( F ` y ) ) e. ran ( ( RR X. { A } ) oF x. F ) ) )
123 122 ralrn 
 |-  ( F Fn RR -> ( A. k e. ran F ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) <-> A. y e. RR ( A x. ( F ` y ) ) e. ran ( ( RR X. { A } ) oF x. F ) ) )
124 94 123 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( A. k e. ran F ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) <-> A. y e. RR ( A x. ( F ` y ) ) e. ran ( ( RR X. { A } ) oF x. F ) ) )
125 120 124 mpbird 
 |-  ( ( ph /\ A =/= 0 ) -> A. k e. ran F ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) )
126 125 r19.21bi 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ran F ) -> ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) )
127 116 126 sylan2 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) )
128 36 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> A e. CC )
129 87 frnd 
 |-  ( ( ph /\ A =/= 0 ) -> ran F C_ RR )
130 129 ssdifssd 
 |-  ( ( ph /\ A =/= 0 ) -> ( ran F \ { 0 } ) C_ RR )
131 130 sselda 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> k e. RR )
132 131 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> k e. CC )
133 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> A =/= 0 )
134 eldifsni 
 |-  ( k e. ( ran F \ { 0 } ) -> k =/= 0 )
135 134 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> k =/= 0 )
136 128 132 133 135 mulne0d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( A x. k ) =/= 0 )
137 eldifsn 
 |-  ( ( A x. k ) e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) <-> ( ( A x. k ) e. ran ( ( RR X. { A } ) oF x. F ) /\ ( A x. k ) =/= 0 ) )
138 127 136 137 sylanbrc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( A x. k ) e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) )
139 simpl 
 |-  ( ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) -> n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) )
140 ssel2 
 |-  ( ( ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) C_ RR /\ n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> n e. RR )
141 32 139 140 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> n e. RR )
142 141 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> n e. CC )
143 2 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> A e. RR )
144 143 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> A e. CC )
145 131 adantrl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> k e. RR )
146 145 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> k e. CC )
147 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> A =/= 0 )
148 142 144 146 147 divmuld 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> ( ( n / A ) = k <-> ( A x. k ) = n ) )
149 148 bicomd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> ( ( A x. k ) = n <-> ( n / A ) = k ) )
150 eqcom 
 |-  ( n = ( A x. k ) <-> ( A x. k ) = n )
151 eqcom 
 |-  ( k = ( n / A ) <-> ( n / A ) = k )
152 149 150 151 3bitr4g 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) /\ k e. ( ran F \ { 0 } ) ) ) -> ( n = ( A x. k ) <-> k = ( n / A ) ) )
153 79 115 138 152 f1o2d 
 |-  ( ( ph /\ A =/= 0 ) -> ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) |-> ( n / A ) ) : ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -1-1-onto-> ( ran F \ { 0 } ) )
154 oveq1 
 |-  ( n = m -> ( n / A ) = ( m / A ) )
155 ovex 
 |-  ( m / A ) e. _V
156 154 79 155 fvmpt 
 |-  ( m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) -> ( ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) |-> ( n / A ) ) ` m ) = ( m / A ) )
157 156 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ) -> ( ( n e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) |-> ( n / A ) ) ` m ) = ( m / A ) )
158 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
159 71 158 sylan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
160 131 159 remulcld 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) e. RR )
161 160 recnd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) e. CC )
162 78 65 153 157 161 fsumf1o 
 |-  ( ( ph /\ A =/= 0 ) -> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) )
163 73 162 eqtrd 
 |-  ( ( ph /\ A =/= 0 ) -> ( S.1 ` F ) = sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) )
164 163 oveq2d 
 |-  ( ( ph /\ A =/= 0 ) -> ( A x. ( S.1 ` F ) ) = ( A x. sum_ m e. ( ran ( ( RR X. { A } ) oF x. F ) \ { 0 } ) ( ( m / A ) x. ( vol ` ( `' F " { ( m / A ) } ) ) ) ) )
165 68 70 164 3eqtr4d 
 |-  ( ( ph /\ A =/= 0 ) -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.1 ` F ) ) )
166 26 165 pm2.61dane 
 |-  ( ph -> ( S.1 ` ( ( RR X. { A } ) oF x. F ) ) = ( A x. ( S.1 ` F ) ) )