Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  meadjiunlem Structured version   Visualization version   GIF version

Theorem meadjiunlem 39358
Description: The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
meadjiunlem.f (𝜑𝑀 ∈ Meas)
meadjiunlem.3 𝑆 = dom 𝑀
meadjiunlem.x (𝜑𝑋𝑉)
meadjiunlem.g (𝜑𝐺:𝑋𝑆)
meadjiunlem.y 𝑌 = {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅}
meadjiunlem.dj (𝜑Disj 𝑖𝑋 (𝐺𝑖))
Assertion
Ref Expression
meadjiunlem (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀𝐺)))
Distinct variable groups:   𝑖,𝐺   𝑖,𝑋   𝑖,𝑌   𝜑,𝑖
Allowed substitution hints:   𝑆(𝑖)   𝑀(𝑖)   𝑉(𝑖)

Proof of Theorem meadjiunlem
Dummy variables 𝑗 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1830 . . . 4 𝑘𝜑
2 meadjiunlem.g . . . . . 6 (𝜑𝐺:𝑋𝑆)
3 meadjiunlem.x . . . . . 6 (𝜑𝑋𝑉)
42, 3jca 553 . . . . 5 (𝜑 → (𝐺:𝑋𝑆𝑋𝑉))
5 fex 6394 . . . . 5 ((𝐺:𝑋𝑆𝑋𝑉) → 𝐺 ∈ V)
6 rnexg 6990 . . . . 5 (𝐺 ∈ V → ran 𝐺 ∈ V)
74, 5, 63syl 18 . . . 4 (𝜑 → ran 𝐺 ∈ V)
8 difssd 3700 . . . 4 (𝜑 → (ran 𝐺 ∖ {∅}) ⊆ ran 𝐺)
9 meadjiunlem.f . . . . . . 7 (𝜑𝑀 ∈ Meas)
10 meadjiunlem.3 . . . . . . 7 𝑆 = dom 𝑀
119, 10meaf 39346 . . . . . 6 (𝜑𝑀:𝑆⟶(0[,]+∞))
1211adantr 480 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑀:𝑆⟶(0[,]+∞))
13 frn 5966 . . . . . . . 8 (𝐺:𝑋𝑆 → ran 𝐺𝑆)
142, 13syl 17 . . . . . . 7 (𝜑 → ran 𝐺𝑆)
1514adantr 480 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → ran 𝐺𝑆)
168sselda 3568 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ ran 𝐺)
1715, 16sseldd 3569 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑘𝑆)
1812, 17ffvelrnd 6268 . . . 4 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → (𝑀𝑘) ∈ (0[,]+∞))
19 simpl 472 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → 𝜑)
20 id 22 . . . . . . . 8 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})))
21 dfin4 3826 . . . . . . . . 9 (ran 𝐺 ∩ {∅}) = (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))
2221eqcomi 2619 . . . . . . . 8 (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) = (ran 𝐺 ∩ {∅})
2320, 22syl6eleq 2698 . . . . . . 7 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ (ran 𝐺 ∩ {∅}))
24 elinel2 3762 . . . . . . . 8 (𝑘 ∈ (ran 𝐺 ∩ {∅}) → 𝑘 ∈ {∅})
25 elsni 4142 . . . . . . . 8 (𝑘 ∈ {∅} → 𝑘 = ∅)
2624, 25syl 17 . . . . . . 7 (𝑘 ∈ (ran 𝐺 ∩ {∅}) → 𝑘 = ∅)
2723, 26syl 17 . . . . . 6 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 = ∅)
2827adantl 481 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → 𝑘 = ∅)
29 simpr 476 . . . . . . 7 ((𝜑𝑘 = ∅) → 𝑘 = ∅)
3029fveq2d 6107 . . . . . 6 ((𝜑𝑘 = ∅) → (𝑀𝑘) = (𝑀‘∅))
319mea0 39347 . . . . . . 7 (𝜑 → (𝑀‘∅) = 0)
3231adantr 480 . . . . . 6 ((𝜑𝑘 = ∅) → (𝑀‘∅) = 0)
3330, 32eqtrd 2644 . . . . 5 ((𝜑𝑘 = ∅) → (𝑀𝑘) = 0)
3419, 28, 33syl2anc 691 . . . 4 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → (𝑀𝑘) = 0)
351, 7, 8, 18, 34sge0ss 39305 . . 3 (𝜑 → (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))) = (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))))
3635eqcomd 2616 . 2 (𝜑 → (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
3711, 14feqresmpt 6160 . . 3 (𝜑 → (𝑀 ↾ ran 𝐺) = (𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘)))
3837fveq2d 6107 . 2 (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))))
392ffvelrnda 6267 . . . . 5 ((𝜑𝑗𝑋) → (𝐺𝑗) ∈ 𝑆)
402feqmptd 6159 . . . . 5 (𝜑𝐺 = (𝑗𝑋 ↦ (𝐺𝑗)))
4111feqmptd 6159 . . . . 5 (𝜑𝑀 = (𝑘𝑆 ↦ (𝑀𝑘)))
42 fveq2 6103 . . . . 5 (𝑘 = (𝐺𝑗) → (𝑀𝑘) = (𝑀‘(𝐺𝑗)))
4339, 40, 41, 42fmptco 6303 . . . 4 (𝜑 → (𝑀𝐺) = (𝑗𝑋 ↦ (𝑀‘(𝐺𝑗))))
4443fveq2d 6107 . . 3 (𝜑 → (Σ^‘(𝑀𝐺)) = (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))))
45 nfv 1830 . . . . 5 𝑗𝜑
46 meadjiunlem.y . . . . . 6 𝑌 = {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅}
47 ssrab2 3650 . . . . . . 7 {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ⊆ 𝑋
4847a1i 11 . . . . . 6 (𝜑 → {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ⊆ 𝑋)
4946, 48syl5eqss 3612 . . . . 5 (𝜑𝑌𝑋)
5011adantr 480 . . . . . 6 ((𝜑𝑗𝑌) → 𝑀:𝑆⟶(0[,]+∞))
512adantr 480 . . . . . . 7 ((𝜑𝑗𝑌) → 𝐺:𝑋𝑆)
5249sselda 3568 . . . . . . 7 ((𝜑𝑗𝑌) → 𝑗𝑋)
5351, 52ffvelrnd 6268 . . . . . 6 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ 𝑆)
5450, 53ffvelrnd 6268 . . . . 5 ((𝜑𝑗𝑌) → (𝑀‘(𝐺𝑗)) ∈ (0[,]+∞))
55 eldifi 3694 . . . . . . . . . . 11 (𝑗 ∈ (𝑋𝑌) → 𝑗𝑋)
5655ad2antlr 759 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗𝑋)
57 fveq2 6103 . . . . . . . . . . . . . . 15 ((𝐺𝑗) = ∅ → (𝑀‘(𝐺𝑗)) = (𝑀‘∅))
5857adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = (𝑀‘∅))
599adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑗) = ∅) → 𝑀 ∈ Meas)
6059mea0 39347 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘∅) = 0)
6158, 60eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = 0)
6261ad4ant14 1285 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = 0)
63 neneq 2788 . . . . . . . . . . . . 13 ((𝑀‘(𝐺𝑗)) ≠ 0 → ¬ (𝑀‘(𝐺𝑗)) = 0)
6463ad2antlr 759 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) ∧ (𝐺𝑗) = ∅) → ¬ (𝑀‘(𝐺𝑗)) = 0)
6562, 64pm2.65da 598 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → ¬ (𝐺𝑗) = ∅)
6665neqned 2789 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → (𝐺𝑗) ≠ ∅)
6756, 66jca 553 . . . . . . . . 9 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → (𝑗𝑋 ∧ (𝐺𝑗) ≠ ∅))
68 fveq2 6103 . . . . . . . . . . 11 (𝑖 = 𝑗 → (𝐺𝑖) = (𝐺𝑗))
6968neeq1d 2841 . . . . . . . . . 10 (𝑖 = 𝑗 → ((𝐺𝑖) ≠ ∅ ↔ (𝐺𝑗) ≠ ∅))
7069elrab 3331 . . . . . . . . 9 (𝑗 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ↔ (𝑗𝑋 ∧ (𝐺𝑗) ≠ ∅))
7167, 70sylibr 223 . . . . . . . 8 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅})
7271, 46syl6eleqr 2699 . . . . . . 7 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗𝑌)
73 eldifn 3695 . . . . . . . 8 (𝑗 ∈ (𝑋𝑌) → ¬ 𝑗𝑌)
7473ad2antlr 759 . . . . . . 7 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → ¬ 𝑗𝑌)
7572, 74pm2.65da 598 . . . . . 6 ((𝜑𝑗 ∈ (𝑋𝑌)) → ¬ (𝑀‘(𝐺𝑗)) ≠ 0)
76 nne 2786 . . . . . 6 (¬ (𝑀‘(𝐺𝑗)) ≠ 0 ↔ (𝑀‘(𝐺𝑗)) = 0)
7775, 76sylib 207 . . . . 5 ((𝜑𝑗 ∈ (𝑋𝑌)) → (𝑀‘(𝐺𝑗)) = 0)
7845, 3, 49, 54, 77sge0ss 39305 . . . 4 (𝜑 → (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))))
7978eqcomd 2616 . . 3 (𝜑 → (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))))
803, 49ssexd 4733 . . . . 5 (𝜑𝑌 ∈ V)
81 nfv 1830 . . . . . . . . 9 𝑖𝜑
82 eqid 2610 . . . . . . . . 9 (𝑖𝑌 ↦ (𝐺𝑖)) = (𝑖𝑌 ↦ (𝐺𝑖))
832ffnd 5959 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
84 dffn3 5967 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋𝐺:𝑋⟶ran 𝐺)
8583, 84sylib 207 . . . . . . . . . . . 12 (𝜑𝐺:𝑋⟶ran 𝐺)
8685adantr 480 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → 𝐺:𝑋⟶ran 𝐺)
8749sselda 3568 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → 𝑖𝑋)
8886, 87ffvelrnd 6268 . . . . . . . . . 10 ((𝜑𝑖𝑌) → (𝐺𝑖) ∈ ran 𝐺)
8946eleq2i 2680 . . . . . . . . . . . . . . 15 (𝑖𝑌𝑖 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅})
90 rabid 3095 . . . . . . . . . . . . . . 15 (𝑖 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ↔ (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9189, 90bitri 263 . . . . . . . . . . . . . 14 (𝑖𝑌 ↔ (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9291biimpi 205 . . . . . . . . . . . . 13 (𝑖𝑌 → (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9392simprd 478 . . . . . . . . . . . 12 (𝑖𝑌 → (𝐺𝑖) ≠ ∅)
9493adantl 481 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → (𝐺𝑖) ≠ ∅)
95 nelsn 4159 . . . . . . . . . . 11 ((𝐺𝑖) ≠ ∅ → ¬ (𝐺𝑖) ∈ {∅})
9694, 95syl 17 . . . . . . . . . 10 ((𝜑𝑖𝑌) → ¬ (𝐺𝑖) ∈ {∅})
9788, 96eldifd 3551 . . . . . . . . 9 ((𝜑𝑖𝑌) → (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}))
98 meadjiunlem.dj . . . . . . . . . 10 (𝜑Disj 𝑖𝑋 (𝐺𝑖))
99 disjss1 4559 . . . . . . . . . 10 (𝑌𝑋 → (Disj 𝑖𝑋 (𝐺𝑖) → Disj 𝑖𝑌 (𝐺𝑖)))
10049, 98, 99sylc 63 . . . . . . . . 9 (𝜑Disj 𝑖𝑌 (𝐺𝑖))
10181, 82, 97, 94, 100disjf1 38364 . . . . . . . 8 (𝜑 → (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅}))
1022, 49feqresmpt 6160 . . . . . . . . 9 (𝜑 → (𝐺𝑌) = (𝑖𝑌 ↦ (𝐺𝑖)))
103 f1eq1 6009 . . . . . . . . 9 ((𝐺𝑌) = (𝑖𝑌 ↦ (𝐺𝑖)) → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ↔ (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅})))
104102, 103syl 17 . . . . . . . 8 (𝜑 → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ↔ (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅})))
105101, 104mpbird 246 . . . . . . 7 (𝜑 → (𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}))
106102rneqd 5274 . . . . . . . . 9 (𝜑 → ran (𝐺𝑌) = ran (𝑖𝑌 ↦ (𝐺𝑖)))
10797ralrimiva 2949 . . . . . . . . . 10 (𝜑 → ∀𝑖𝑌 (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}))
10882rnmptss 6299 . . . . . . . . . 10 (∀𝑖𝑌 (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}) → ran (𝑖𝑌 ↦ (𝐺𝑖)) ⊆ (ran 𝐺 ∖ {∅}))
109107, 108syl 17 . . . . . . . . 9 (𝜑 → ran (𝑖𝑌 ↦ (𝐺𝑖)) ⊆ (ran 𝐺 ∖ {∅}))
110106, 109eqsstrd 3602 . . . . . . . 8 (𝜑 → ran (𝐺𝑌) ⊆ (ran 𝐺 ∖ {∅}))
111 simpl 472 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝜑)
112 eldifi 3694 . . . . . . . . . . . 12 (𝑥 ∈ (ran 𝐺 ∖ {∅}) → 𝑥 ∈ ran 𝐺)
113112adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ∈ ran 𝐺)
114 eldifsni 4261 . . . . . . . . . . . 12 (𝑥 ∈ (ran 𝐺 ∖ {∅}) → 𝑥 ≠ ∅)
115114adantl 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ≠ ∅)
116 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
117 fvelrnb 6153 . . . . . . . . . . . . . . . 16 (𝐺 Fn 𝑋 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
11883, 117syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
119118adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ran 𝐺) → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
120116, 119mpbid 221 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ran 𝐺) → ∃𝑖𝑋 (𝐺𝑖) = 𝑥)
1211203adant3 1074 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → ∃𝑖𝑋 (𝐺𝑖) = 𝑥)
122 id 22 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑖) = 𝑥 → (𝐺𝑖) = 𝑥)
123122eqcomd 2616 . . . . . . . . . . . . . . . . 17 ((𝐺𝑖) = 𝑥𝑥 = (𝐺𝑖))
1241233ad2ant3 1077 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑥 = (𝐺𝑖))
125 simp1l 1078 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝜑)
126 simp2 1055 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑖𝑋)
127 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) = 𝑥)
128 simpl 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → 𝑥 ≠ ∅)
129127, 128eqnetrd 2849 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
130129adantll 746 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ≠ ∅) ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
1311303adant2 1073 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
13291biimpri 217 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → 𝑖𝑌)
133 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑖) ∈ V
134133a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ V)
13582elrnmpt1 5295 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑌 ∧ (𝐺𝑖) ∈ V) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
136132, 134, 135syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
1371363adant1 1072 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
138106eqcomd 2616 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑖𝑌 ↦ (𝐺𝑖)) = ran (𝐺𝑌))
1391383ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → ran (𝑖𝑌 ↦ (𝐺𝑖)) = ran (𝐺𝑌))
140137, 139eleqtrd 2690 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝐺𝑌))
141125, 126, 131, 140syl3anc 1318 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ∈ ran (𝐺𝑌))
142124, 141eqeltrd 2688 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑥 ∈ ran (𝐺𝑌))
1431423exp 1256 . . . . . . . . . . . . . 14 ((𝜑𝑥 ≠ ∅) → (𝑖𝑋 → ((𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌))))
144143rexlimdv 3012 . . . . . . . . . . . . 13 ((𝜑𝑥 ≠ ∅) → (∃𝑖𝑋 (𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌)))
1451443adant2 1073 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → (∃𝑖𝑋 (𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌)))
146121, 145mpd 15 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → 𝑥 ∈ ran (𝐺𝑌))
147111, 113, 115, 146syl3anc 1318 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ∈ ran (𝐺𝑌))
148147ralrimiva 2949 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (ran 𝐺 ∖ {∅})𝑥 ∈ ran (𝐺𝑌))
149 dfss3 3558 . . . . . . . . 9 ((ran 𝐺 ∖ {∅}) ⊆ ran (𝐺𝑌) ↔ ∀𝑥 ∈ (ran 𝐺 ∖ {∅})𝑥 ∈ ran (𝐺𝑌))
150148, 149sylibr 223 . . . . . . . 8 (𝜑 → (ran 𝐺 ∖ {∅}) ⊆ ran (𝐺𝑌))
151110, 150eqssd 3585 . . . . . . 7 (𝜑 → ran (𝐺𝑌) = (ran 𝐺 ∖ {∅}))
152105, 151jca 553 . . . . . 6 (𝜑 → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ∧ ran (𝐺𝑌) = (ran 𝐺 ∖ {∅})))
153 dff1o5 6059 . . . . . 6 ((𝐺𝑌):𝑌1-1-onto→(ran 𝐺 ∖ {∅}) ↔ ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ∧ ran (𝐺𝑌) = (ran 𝐺 ∖ {∅})))
154152, 153sylibr 223 . . . . 5 (𝜑 → (𝐺𝑌):𝑌1-1-onto→(ran 𝐺 ∖ {∅}))
155 fvres 6117 . . . . . 6 (𝑗𝑌 → ((𝐺𝑌)‘𝑗) = (𝐺𝑗))
156155adantl 481 . . . . 5 ((𝜑𝑗𝑌) → ((𝐺𝑌)‘𝑗) = (𝐺𝑗))
1571, 45, 42, 80, 154, 156, 18sge0f1o 39275 . . . 4 (𝜑 → (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))) = (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))))
158157eqcomd 2616 . . 3 (𝜑 → (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
15944, 79, 1583eqtrd 2648 . 2 (𝜑 → (Σ^‘(𝑀𝐺)) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
16036, 38, 1593eqtr4d 2654 1 (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wrex 2897  {crab 2900  Vcvv 3173  cdif 3537  cin 3539  wss 3540  c0 3874  {csn 4125  Disj wdisj 4553  cmpt 4643  dom cdm 5038  ran crn 5039  cres 5040  ccom 5042   Fn wfn 5799  wf 5800  1-1wf1 5801  1-1-ontowf1o 5803  cfv 5804  (class class class)co 6549  0cc0 9815  +∞cpnf 9950  [,]cicc 12049  Σ^csumge0 39255  Meascmea 39342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xadd 11823  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-sumge0 39256  df-mea 39343
This theorem is referenced by:  meadjiun  39359
  Copyright terms: Public domain W3C validator