MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  i1fadd Structured version   Visualization version   GIF version

Theorem i1fadd 23899
Description: The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypotheses
Ref Expression
i1fadd.1 (𝜑𝐹 ∈ dom ∫1)
i1fadd.2 (𝜑𝐺 ∈ dom ∫1)
Assertion
Ref Expression
i1fadd (𝜑 → (𝐹𝑓 + 𝐺) ∈ dom ∫1)

Proof of Theorem i1fadd
Dummy variables 𝑦 𝑧 𝑤 𝑣 𝑥 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 readdcl 10355 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
21adantl 475 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
3 i1fadd.1 . . . 4 (𝜑𝐹 ∈ dom ∫1)
4 i1ff 23880 . . . 4 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
53, 4syl 17 . . 3 (𝜑𝐹:ℝ⟶ℝ)
6 i1fadd.2 . . . 4 (𝜑𝐺 ∈ dom ∫1)
7 i1ff 23880 . . . 4 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
86, 7syl 17 . . 3 (𝜑𝐺:ℝ⟶ℝ)
9 reex 10363 . . . 4 ℝ ∈ V
109a1i 11 . . 3 (𝜑 → ℝ ∈ V)
11 inidm 4042 . . 3 (ℝ ∩ ℝ) = ℝ
122, 5, 8, 10, 10, 11off 7189 . 2 (𝜑 → (𝐹𝑓 + 𝐺):ℝ⟶ℝ)
13 i1frn 23881 . . . . . 6 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
143, 13syl 17 . . . . 5 (𝜑 → ran 𝐹 ∈ Fin)
15 i1frn 23881 . . . . . 6 (𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin)
166, 15syl 17 . . . . 5 (𝜑 → ran 𝐺 ∈ Fin)
17 xpfi 8519 . . . . 5 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
1814, 16, 17syl2anc 579 . . . 4 (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
19 eqid 2777 . . . . . 6 (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))
20 ovex 6954 . . . . . 6 (𝑢 + 𝑣) ∈ V
2119, 20fnmpt2i 7519 . . . . 5 (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺)
22 dffn4 6372 . . . . 5 ((𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) ↔ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)))
2321, 22mpbi 222 . . . 4 (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))
24 fofi 8540 . . . 4 (((ran 𝐹 × ran 𝐺) ∈ Fin ∧ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin)
2518, 23, 24sylancl 580 . . 3 (𝜑 → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin)
26 eqid 2777 . . . . . . . . 9 (𝑥 + 𝑦) = (𝑥 + 𝑦)
27 rspceov 6968 . . . . . . . . 9 ((𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺 ∧ (𝑥 + 𝑦) = (𝑥 + 𝑦)) → ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))
2826, 27mp3an3 1523 . . . . . . . 8 ((𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))
29 ovex 6954 . . . . . . . . 9 (𝑥 + 𝑦) ∈ V
30 eqeq1 2781 . . . . . . . . . 10 (𝑤 = (𝑥 + 𝑦) → (𝑤 = (𝑢 + 𝑣) ↔ (𝑥 + 𝑦) = (𝑢 + 𝑣)))
31302rexbidv 3241 . . . . . . . . 9 (𝑤 = (𝑥 + 𝑦) → (∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)))
3229, 31elab 3557 . . . . . . . 8 ((𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} ↔ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))
3328, 32sylibr 226 . . . . . . 7 ((𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)})
3433adantl 475 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)})
355ffnd 6292 . . . . . . 7 (𝜑𝐹 Fn ℝ)
36 dffn3 6302 . . . . . . 7 (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
3735, 36sylib 210 . . . . . 6 (𝜑𝐹:ℝ⟶ran 𝐹)
388ffnd 6292 . . . . . . 7 (𝜑𝐺 Fn ℝ)
39 dffn3 6302 . . . . . . 7 (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
4038, 39sylib 210 . . . . . 6 (𝜑𝐺:ℝ⟶ran 𝐺)
4134, 37, 40, 10, 10, 11off 7189 . . . . 5 (𝜑 → (𝐹𝑓 + 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)})
4241frnd 6298 . . . 4 (𝜑 → ran (𝐹𝑓 + 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)})
4319rnmpt2 7047 . . . 4 ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}
4442, 43syl6sseqr 3870 . . 3 (𝜑 → ran (𝐹𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)))
45 ssfi 8468 . . 3 ((ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) ∈ Fin ∧ ran (𝐹𝑓 + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) → ran (𝐹𝑓 + 𝐺) ∈ Fin)
4625, 44, 45syl2anc 579 . 2 (𝜑 → ran (𝐹𝑓 + 𝐺) ∈ Fin)
4712frnd 6298 . . . . . . 7 (𝜑 → ran (𝐹𝑓 + 𝐺) ⊆ ℝ)
4847ssdifssd 3970 . . . . . 6 (𝜑 → (ran (𝐹𝑓 + 𝐺) ∖ {0}) ⊆ ℝ)
4948sselda 3820 . . . . 5 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈ ℝ)
5049recnd 10405 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → 𝑦 ∈ ℂ)
513, 6i1faddlem 23897 . . . 4 ((𝜑𝑦 ∈ ℂ) → ((𝐹𝑓 + 𝐺) “ {𝑦}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})))
5250, 51syldan 585 . . 3 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ((𝐹𝑓 + 𝐺) “ {𝑦}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})))
5316adantr 474 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ∈ Fin)
543ad2antrr 716 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ dom ∫1)
55 i1fmbf 23879 . . . . . . . 8 (𝐹 ∈ dom ∫1𝐹 ∈ MblFn)
5654, 55syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ MblFn)
575ad2antrr 716 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹:ℝ⟶ℝ)
5812ad2antrr 716 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐹𝑓 + 𝐺):ℝ⟶ℝ)
5958frnd 6298 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ran (𝐹𝑓 + 𝐺) ⊆ ℝ)
60 eldifi 3954 . . . . . . . . . 10 (𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0}) → 𝑦 ∈ ran (𝐹𝑓 + 𝐺))
6160ad2antlr 717 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ran (𝐹𝑓 + 𝐺))
6259, 61sseldd 3821 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ℝ)
638adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → 𝐺:ℝ⟶ℝ)
6463frnd 6298 . . . . . . . . 9 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ran 𝐺 ⊆ ℝ)
6564sselda 3820 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
6662, 65resubcld 10803 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑦𝑧) ∈ ℝ)
67 mbfimasn 23836 . . . . . . 7 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ (𝑦𝑧) ∈ ℝ) → (𝐹 “ {(𝑦𝑧)}) ∈ dom vol)
6856, 57, 66, 67syl3anc 1439 . . . . . 6 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐹 “ {(𝑦𝑧)}) ∈ dom vol)
696ad2antrr 716 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ dom ∫1)
70 i1fmbf 23879 . . . . . . . 8 (𝐺 ∈ dom ∫1𝐺 ∈ MblFn)
7169, 70syl 17 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ MblFn)
728ad2antrr 716 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺:ℝ⟶ℝ)
73 mbfimasn 23836 . . . . . . 7 ((𝐺 ∈ MblFn ∧ 𝐺:ℝ⟶ℝ ∧ 𝑧 ∈ ℝ) → (𝐺 “ {𝑧}) ∈ dom vol)
7471, 72, 65, 73syl3anc 1439 . . . . . 6 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐺 “ {𝑧}) ∈ dom vol)
75 inmbl 23746 . . . . . 6 (((𝐹 “ {(𝑦𝑧)}) ∈ dom vol ∧ (𝐺 “ {𝑧}) ∈ dom vol) → ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
7668, 74, 75syl2anc 579 . . . . 5 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
7776ralrimiva 3147 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ∀𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
78 finiunmbl 23748 . . . 4 ((ran 𝐺 ∈ Fin ∧ ∀𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol) → 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
7953, 77, 78syl2anc 579 . . 3 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8052, 79eqeltrd 2858 . 2 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ((𝐹𝑓 + 𝐺) “ {𝑦}) ∈ dom vol)
81 mblvol 23734 . . . 4 (((𝐹𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → (vol‘((𝐹𝑓 + 𝐺) “ {𝑦})) = (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})))
8280, 81syl 17 . . 3 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol‘((𝐹𝑓 + 𝐺) “ {𝑦})) = (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})))
83 mblss 23735 . . . . 5 (((𝐹𝑓 + 𝐺) “ {𝑦}) ∈ dom vol → ((𝐹𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ)
8480, 83syl 17 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ((𝐹𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ)
85 inss1 4052 . . . . . . . . 9 ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐹 “ {(𝑦𝑧)})
8685a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐹 “ {(𝑦𝑧)}))
8768adantrr 707 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝐹 “ {(𝑦𝑧)}) ∈ dom vol)
88 mblss 23735 . . . . . . . . 9 ((𝐹 “ {(𝑦𝑧)}) ∈ dom vol → (𝐹 “ {(𝑦𝑧)}) ⊆ ℝ)
8987, 88syl 17 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝐹 “ {(𝑦𝑧)}) ⊆ ℝ)
90 mblvol 23734 . . . . . . . . . 10 ((𝐹 “ {(𝑦𝑧)}) ∈ dom vol → (vol‘(𝐹 “ {(𝑦𝑧)})) = (vol*‘(𝐹 “ {(𝑦𝑧)})))
9187, 90syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol‘(𝐹 “ {(𝑦𝑧)})) = (vol*‘(𝐹 “ {(𝑦𝑧)})))
92 simprr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → 𝑧 = 0)
9392oveq2d 6938 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝑦𝑧) = (𝑦 − 0))
9450adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → 𝑦 ∈ ℂ)
9594subid1d 10723 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝑦 − 0) = 𝑦)
9693, 95eqtrd 2813 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝑦𝑧) = 𝑦)
9796sneqd 4409 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → {(𝑦𝑧)} = {𝑦})
9897imaeq2d 5720 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (𝐹 “ {(𝑦𝑧)}) = (𝐹 “ {𝑦}))
9998fveq2d 6450 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol‘(𝐹 “ {(𝑦𝑧)})) = (vol‘(𝐹 “ {𝑦})))
100 i1fima2sn 23884 . . . . . . . . . . . 12 ((𝐹 ∈ dom ∫1𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol‘(𝐹 “ {𝑦})) ∈ ℝ)
1013, 100sylan 575 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol‘(𝐹 “ {𝑦})) ∈ ℝ)
102101adantr 474 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol‘(𝐹 “ {𝑦})) ∈ ℝ)
10399, 102eqeltrd 2858 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol‘(𝐹 “ {(𝑦𝑧)})) ∈ ℝ)
10491, 103eqeltrrd 2859 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol*‘(𝐹 “ {(𝑦𝑧)})) ∈ ℝ)
105 ovolsscl 23690 . . . . . . . 8 ((((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐹 “ {(𝑦𝑧)}) ∧ (𝐹 “ {(𝑦𝑧)}) ⊆ ℝ ∧ (vol*‘(𝐹 “ {(𝑦𝑧)})) ∈ ℝ) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
10686, 89, 104, 105syl3anc 1439 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 = 0)) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
107106expr 450 . . . . . 6 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 = 0 → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ))
108 eldifsn 4549 . . . . . . . 8 (𝑧 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑧 ∈ ran 𝐺𝑧 ≠ 0))
109 inss2 4053 . . . . . . . . . 10 ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧})
110109a1i 11 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧}))
111 eldifi 3954 . . . . . . . . . 10 (𝑧 ∈ (ran 𝐺 ∖ {0}) → 𝑧 ∈ ran 𝐺)
112 mblss 23735 . . . . . . . . . . 11 ((𝐺 “ {𝑧}) ∈ dom vol → (𝐺 “ {𝑧}) ⊆ ℝ)
11374, 112syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐺 “ {𝑧}) ⊆ ℝ)
114111, 113sylan2 586 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (𝐺 “ {𝑧}) ⊆ ℝ)
115 i1fima 23882 . . . . . . . . . . . . 13 (𝐺 ∈ dom ∫1 → (𝐺 “ {𝑧}) ∈ dom vol)
1166, 115syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐺 “ {𝑧}) ∈ dom vol)
117116ad2antrr 716 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (𝐺 “ {𝑧}) ∈ dom vol)
118 mblvol 23734 . . . . . . . . . . 11 ((𝐺 “ {𝑧}) ∈ dom vol → (vol‘(𝐺 “ {𝑧})) = (vol*‘(𝐺 “ {𝑧})))
119117, 118syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(𝐺 “ {𝑧})) = (vol*‘(𝐺 “ {𝑧})))
1206adantr 474 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → 𝐺 ∈ dom ∫1)
121 i1fima2sn 23884 . . . . . . . . . . 11 ((𝐺 ∈ dom ∫1𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(𝐺 “ {𝑧})) ∈ ℝ)
122120, 121sylan 575 . . . . . . . . . 10 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(𝐺 “ {𝑧})) ∈ ℝ)
123119, 122eqeltrrd 2859 . . . . . . . . 9 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(𝐺 “ {𝑧})) ∈ ℝ)
124 ovolsscl 23690 . . . . . . . . 9 ((((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧}) ∧ (𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(𝐺 “ {𝑧})) ∈ ℝ) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
125110, 114, 123, 124syl3anc 1439 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
126108, 125sylan2br 588 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺𝑧 ≠ 0)) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
127126expr 450 . . . . . 6 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ≠ 0 → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ))
128107, 127pm2.61dne 3055 . . . . 5 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
12953, 128fsumrecl 14872 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
13052fveq2d 6450 . . . . 5 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})) = (vol*‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))))
131109, 113syl5ss 3831 . . . . . . . 8 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ ℝ)
132131, 128jca 507 . . . . . . 7 (((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ))
133132ralrimiva 3147 . . . . . 6 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → ∀𝑧 ∈ ran 𝐺(((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ))
134 ovolfiniun 23705 . . . . . 6 ((ran 𝐺 ∈ Fin ∧ ∀𝑧 ∈ ran 𝐺(((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)) → (vol*‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))))
13553, 133, 134syl2anc 579 . . . . 5 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol*‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))))
136130, 135eqbrtrd 4908 . . . 4 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))))
137 ovollecl 23687 . . . 4 ((((𝐹𝑓 + 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((𝐹 “ {(𝑦𝑧)}) ∩ (𝐺 “ {𝑧})))) → (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})) ∈ ℝ)
13884, 129, 136, 137syl3anc 1439 . . 3 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol*‘((𝐹𝑓 + 𝐺) “ {𝑦})) ∈ ℝ)
13982, 138eqeltrd 2858 . 2 ((𝜑𝑦 ∈ (ran (𝐹𝑓 + 𝐺) ∖ {0})) → (vol‘((𝐹𝑓 + 𝐺) “ {𝑦})) ∈ ℝ)
14012, 46, 80, 139i1fd 23885 1 (𝜑 → (𝐹𝑓 + 𝐺) ∈ dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2106  {cab 2762  wne 2968  wral 3089  wrex 3090  Vcvv 3397  cdif 3788  cin 3790  wss 3791  {csn 4397   ciun 4753   class class class wbr 4886   × cxp 5353  ccnv 5354  dom cdm 5355  ran crn 5356  cima 5358   Fn wfn 6130  wf 6131  ontowfo 6133  cfv 6135  (class class class)co 6922  cmpt2 6924  𝑓 cof 7172  Fincfn 8241  cc 10270  cr 10271  0cc0 10272   + caddc 10275  cle 10412  cmin 10606  Σcsu 14824  vol*covol 23666  volcvol 23667  MblFncmbf 23818  1citg1 23819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-q 12096  df-rp 12138  df-xadd 12258  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-sum 14825  df-xmet 20135  df-met 20136  df-ovol 23668  df-vol 23669  df-mbf 23823  df-itg1 23824
This theorem is referenced by:  itg1addlem4  23903  i1fsub  23912  itg2splitlem  23952  itg2split  23953  itg2addlem  23962  itg2addnc  34073  ftc1anclem3  34096  ftc1anclem5  34098  ftc1anclem8  34101
  Copyright terms: Public domain W3C validator