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 ( 𝜑𝐹 ∈ dom ∫1 )
i1fmulc.3 ( 𝜑𝐴 ∈ ℝ )
Assertion itg1mulc ( 𝜑 → ( ∫1 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫1𝐹 ) ) )

Proof

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