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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 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 ‘ 𝐹 ) ) )