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 41204
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 1993 . . . 4 𝑘𝜑
2 meadjiunlem.g . . . . . 6 (𝜑𝐺:𝑋𝑆)
3 meadjiunlem.x . . . . . 6 (𝜑𝑋𝑉)
42, 3jca 555 . . . . 5 (𝜑 → (𝐺:𝑋𝑆𝑋𝑉))
5 fex 6655 . . . . 5 ((𝐺:𝑋𝑆𝑋𝑉) → 𝐺 ∈ V)
6 rnexg 7265 . . . . 5 (𝐺 ∈ V → ran 𝐺 ∈ V)
74, 5, 63syl 18 . . . 4 (𝜑 → ran 𝐺 ∈ V)
8 difssd 3882 . . . 4 (𝜑 → (ran 𝐺 ∖ {∅}) ⊆ ran 𝐺)
9 meadjiunlem.f . . . . . . 7 (𝜑𝑀 ∈ Meas)
10 meadjiunlem.3 . . . . . . 7 𝑆 = dom 𝑀
119, 10meaf 41192 . . . . . 6 (𝜑𝑀:𝑆⟶(0[,]+∞))
1211adantr 472 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑀:𝑆⟶(0[,]+∞))
13 frn 6215 . . . . . . . 8 (𝐺:𝑋𝑆 → ran 𝐺𝑆)
142, 13syl 17 . . . . . . 7 (𝜑 → ran 𝐺𝑆)
1514adantr 472 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → ran 𝐺𝑆)
168sselda 3745 . . . . . 6 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ ran 𝐺)
1715, 16sseldd 3746 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → 𝑘𝑆)
1812, 17ffvelrnd 6525 . . . 4 ((𝜑𝑘 ∈ (ran 𝐺 ∖ {∅})) → (𝑀𝑘) ∈ (0[,]+∞))
19 simpl 474 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → 𝜑)
20 id 22 . . . . . . . 8 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})))
21 dfin4 4011 . . . . . . . . 9 (ran 𝐺 ∩ {∅}) = (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))
2221eqcomi 2770 . . . . . . . 8 (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) = (ran 𝐺 ∩ {∅})
2320, 22syl6eleq 2850 . . . . . . 7 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 ∈ (ran 𝐺 ∩ {∅}))
24 elinel2 3944 . . . . . . . 8 (𝑘 ∈ (ran 𝐺 ∩ {∅}) → 𝑘 ∈ {∅})
25 elsni 4339 . . . . . . . 8 (𝑘 ∈ {∅} → 𝑘 = ∅)
2624, 25syl 17 . . . . . . 7 (𝑘 ∈ (ran 𝐺 ∩ {∅}) → 𝑘 = ∅)
2723, 26syl 17 . . . . . 6 (𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅})) → 𝑘 = ∅)
2827adantl 473 . . . . 5 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → 𝑘 = ∅)
29 simpr 479 . . . . . . 7 ((𝜑𝑘 = ∅) → 𝑘 = ∅)
3029fveq2d 6358 . . . . . 6 ((𝜑𝑘 = ∅) → (𝑀𝑘) = (𝑀‘∅))
319mea0 41193 . . . . . . 7 (𝜑 → (𝑀‘∅) = 0)
3231adantr 472 . . . . . 6 ((𝜑𝑘 = ∅) → (𝑀‘∅) = 0)
3330, 32eqtrd 2795 . . . . 5 ((𝜑𝑘 = ∅) → (𝑀𝑘) = 0)
3419, 28, 33syl2anc 696 . . . 4 ((𝜑𝑘 ∈ (ran 𝐺 ∖ (ran 𝐺 ∖ {∅}))) → (𝑀𝑘) = 0)
351, 7, 8, 18, 34sge0ss 41151 . . 3 (𝜑 → (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))) = (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))))
3635eqcomd 2767 . 2 (𝜑 → (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
3711, 14feqresmpt 6414 . . 3 (𝜑 → (𝑀 ↾ ran 𝐺) = (𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘)))
3837fveq2d 6358 . 2 (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑘 ∈ ran 𝐺 ↦ (𝑀𝑘))))
392ffvelrnda 6524 . . . . 5 ((𝜑𝑗𝑋) → (𝐺𝑗) ∈ 𝑆)
402feqmptd 6413 . . . . 5 (𝜑𝐺 = (𝑗𝑋 ↦ (𝐺𝑗)))
4111feqmptd 6413 . . . . 5 (𝜑𝑀 = (𝑘𝑆 ↦ (𝑀𝑘)))
42 fveq2 6354 . . . . 5 (𝑘 = (𝐺𝑗) → (𝑀𝑘) = (𝑀‘(𝐺𝑗)))
4339, 40, 41, 42fmptco 6561 . . . 4 (𝜑 → (𝑀𝐺) = (𝑗𝑋 ↦ (𝑀‘(𝐺𝑗))))
4443fveq2d 6358 . . 3 (𝜑 → (Σ^‘(𝑀𝐺)) = (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))))
45 nfv 1993 . . . . 5 𝑗𝜑
46 meadjiunlem.y . . . . . 6 𝑌 = {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅}
47 ssrab2 3829 . . . . . . 7 {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ⊆ 𝑋
4847a1i 11 . . . . . 6 (𝜑 → {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ⊆ 𝑋)
4946, 48syl5eqss 3791 . . . . 5 (𝜑𝑌𝑋)
5011adantr 472 . . . . . 6 ((𝜑𝑗𝑌) → 𝑀:𝑆⟶(0[,]+∞))
512adantr 472 . . . . . . 7 ((𝜑𝑗𝑌) → 𝐺:𝑋𝑆)
5249sselda 3745 . . . . . . 7 ((𝜑𝑗𝑌) → 𝑗𝑋)
5351, 52ffvelrnd 6525 . . . . . 6 ((𝜑𝑗𝑌) → (𝐺𝑗) ∈ 𝑆)
5450, 53ffvelrnd 6525 . . . . 5 ((𝜑𝑗𝑌) → (𝑀‘(𝐺𝑗)) ∈ (0[,]+∞))
55 eldifi 3876 . . . . . . . . . . 11 (𝑗 ∈ (𝑋𝑌) → 𝑗𝑋)
5655ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗𝑋)
57 fveq2 6354 . . . . . . . . . . . . . . 15 ((𝐺𝑗) = ∅ → (𝑀‘(𝐺𝑗)) = (𝑀‘∅))
5857adantl 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = (𝑀‘∅))
599adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑗) = ∅) → 𝑀 ∈ Meas)
6059mea0 41193 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘∅) = 0)
6158, 60eqtrd 2795 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = 0)
6261ad4ant14 1209 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) ∧ (𝐺𝑗) = ∅) → (𝑀‘(𝐺𝑗)) = 0)
63 neneq 2939 . . . . . . . . . . . . 13 ((𝑀‘(𝐺𝑗)) ≠ 0 → ¬ (𝑀‘(𝐺𝑗)) = 0)
6463ad2antlr 765 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) ∧ (𝐺𝑗) = ∅) → ¬ (𝑀‘(𝐺𝑗)) = 0)
6562, 64pm2.65da 601 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → ¬ (𝐺𝑗) = ∅)
6665neqned 2940 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → (𝐺𝑗) ≠ ∅)
6756, 66jca 555 . . . . . . . . 9 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → (𝑗𝑋 ∧ (𝐺𝑗) ≠ ∅))
68 fveq2 6354 . . . . . . . . . . 11 (𝑖 = 𝑗 → (𝐺𝑖) = (𝐺𝑗))
6968neeq1d 2992 . . . . . . . . . 10 (𝑖 = 𝑗 → ((𝐺𝑖) ≠ ∅ ↔ (𝐺𝑗) ≠ ∅))
7069elrab 3505 . . . . . . . . 9 (𝑗 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ↔ (𝑗𝑋 ∧ (𝐺𝑗) ≠ ∅))
7167, 70sylibr 224 . . . . . . . 8 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅})
7271, 46syl6eleqr 2851 . . . . . . 7 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → 𝑗𝑌)
73 eldifn 3877 . . . . . . . 8 (𝑗 ∈ (𝑋𝑌) → ¬ 𝑗𝑌)
7473ad2antlr 765 . . . . . . 7 (((𝜑𝑗 ∈ (𝑋𝑌)) ∧ (𝑀‘(𝐺𝑗)) ≠ 0) → ¬ 𝑗𝑌)
7572, 74pm2.65da 601 . . . . . 6 ((𝜑𝑗 ∈ (𝑋𝑌)) → ¬ (𝑀‘(𝐺𝑗)) ≠ 0)
76 nne 2937 . . . . . 6 (¬ (𝑀‘(𝐺𝑗)) ≠ 0 ↔ (𝑀‘(𝐺𝑗)) = 0)
7775, 76sylib 208 . . . . 5 ((𝜑𝑗 ∈ (𝑋𝑌)) → (𝑀‘(𝐺𝑗)) = 0)
7845, 3, 49, 54, 77sge0ss 41151 . . . 4 (𝜑 → (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))))
7978eqcomd 2767 . . 3 (𝜑 → (Σ^‘(𝑗𝑋 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))))
803, 49ssexd 4958 . . . . 5 (𝜑𝑌 ∈ V)
81 nfv 1993 . . . . . . . . 9 𝑖𝜑
82 eqid 2761 . . . . . . . . 9 (𝑖𝑌 ↦ (𝐺𝑖)) = (𝑖𝑌 ↦ (𝐺𝑖))
832ffnd 6208 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
84 dffn3 6216 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋𝐺:𝑋⟶ran 𝐺)
8583, 84sylib 208 . . . . . . . . . . . 12 (𝜑𝐺:𝑋⟶ran 𝐺)
8685adantr 472 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → 𝐺:𝑋⟶ran 𝐺)
8749sselda 3745 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → 𝑖𝑋)
8886, 87ffvelrnd 6525 . . . . . . . . . 10 ((𝜑𝑖𝑌) → (𝐺𝑖) ∈ ran 𝐺)
8946eleq2i 2832 . . . . . . . . . . . . . . 15 (𝑖𝑌𝑖 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅})
90 rabid 3255 . . . . . . . . . . . . . . 15 (𝑖 ∈ {𝑖𝑋 ∣ (𝐺𝑖) ≠ ∅} ↔ (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9189, 90bitri 264 . . . . . . . . . . . . . 14 (𝑖𝑌 ↔ (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9291biimpi 206 . . . . . . . . . . . . 13 (𝑖𝑌 → (𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅))
9392simprd 482 . . . . . . . . . . . 12 (𝑖𝑌 → (𝐺𝑖) ≠ ∅)
9493adantl 473 . . . . . . . . . . 11 ((𝜑𝑖𝑌) → (𝐺𝑖) ≠ ∅)
95 nelsn 4358 . . . . . . . . . . 11 ((𝐺𝑖) ≠ ∅ → ¬ (𝐺𝑖) ∈ {∅})
9694, 95syl 17 . . . . . . . . . 10 ((𝜑𝑖𝑌) → ¬ (𝐺𝑖) ∈ {∅})
9788, 96eldifd 3727 . . . . . . . . 9 ((𝜑𝑖𝑌) → (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}))
98 meadjiunlem.dj . . . . . . . . . 10 (𝜑Disj 𝑖𝑋 (𝐺𝑖))
99 disjss1 4779 . . . . . . . . . 10 (𝑌𝑋 → (Disj 𝑖𝑋 (𝐺𝑖) → Disj 𝑖𝑌 (𝐺𝑖)))
10049, 98, 99sylc 65 . . . . . . . . 9 (𝜑Disj 𝑖𝑌 (𝐺𝑖))
10181, 82, 97, 94, 100disjf1 39887 . . . . . . . 8 (𝜑 → (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅}))
1022, 49feqresmpt 6414 . . . . . . . . 9 (𝜑 → (𝐺𝑌) = (𝑖𝑌 ↦ (𝐺𝑖)))
103 f1eq1 6258 . . . . . . . . 9 ((𝐺𝑌) = (𝑖𝑌 ↦ (𝐺𝑖)) → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ↔ (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅})))
104102, 103syl 17 . . . . . . . 8 (𝜑 → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ↔ (𝑖𝑌 ↦ (𝐺𝑖)):𝑌1-1→(ran 𝐺 ∖ {∅})))
105101, 104mpbird 247 . . . . . . 7 (𝜑 → (𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}))
106102rneqd 5509 . . . . . . . . 9 (𝜑 → ran (𝐺𝑌) = ran (𝑖𝑌 ↦ (𝐺𝑖)))
10797ralrimiva 3105 . . . . . . . . . 10 (𝜑 → ∀𝑖𝑌 (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}))
10882rnmptss 6557 . . . . . . . . . 10 (∀𝑖𝑌 (𝐺𝑖) ∈ (ran 𝐺 ∖ {∅}) → ran (𝑖𝑌 ↦ (𝐺𝑖)) ⊆ (ran 𝐺 ∖ {∅}))
109107, 108syl 17 . . . . . . . . 9 (𝜑 → ran (𝑖𝑌 ↦ (𝐺𝑖)) ⊆ (ran 𝐺 ∖ {∅}))
110106, 109eqsstrd 3781 . . . . . . . 8 (𝜑 → ran (𝐺𝑌) ⊆ (ran 𝐺 ∖ {∅}))
111 simpl 474 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝜑)
112 eldifi 3876 . . . . . . . . . . . 12 (𝑥 ∈ (ran 𝐺 ∖ {∅}) → 𝑥 ∈ ran 𝐺)
113112adantl 473 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ∈ ran 𝐺)
114 eldifsni 4467 . . . . . . . . . . . 12 (𝑥 ∈ (ran 𝐺 ∖ {∅}) → 𝑥 ≠ ∅)
115114adantl 473 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ≠ ∅)
116 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ran 𝐺) → 𝑥 ∈ ran 𝐺)
117 fvelrnb 6407 . . . . . . . . . . . . . . . 16 (𝐺 Fn 𝑋 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
11883, 117syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
119118adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ran 𝐺) → (𝑥 ∈ ran 𝐺 ↔ ∃𝑖𝑋 (𝐺𝑖) = 𝑥))
120116, 119mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ran 𝐺) → ∃𝑖𝑋 (𝐺𝑖) = 𝑥)
1211203adant3 1127 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → ∃𝑖𝑋 (𝐺𝑖) = 𝑥)
122 id 22 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑖) = 𝑥 → (𝐺𝑖) = 𝑥)
123122eqcomd 2767 . . . . . . . . . . . . . . . . 17 ((𝐺𝑖) = 𝑥𝑥 = (𝐺𝑖))
1241233ad2ant3 1130 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑥 = (𝐺𝑖))
125 simp1l 1240 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝜑)
126 simp2 1132 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑖𝑋)
127 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) = 𝑥)
128 simpl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → 𝑥 ≠ ∅)
129127, 128eqnetrd 3000 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ≠ ∅ ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
130129adantll 752 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ≠ ∅) ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
1311303adant2 1126 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ≠ ∅)
13291biimpri 218 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → 𝑖𝑌)
133 fvexd 6366 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ V)
13482elrnmpt1 5530 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑌 ∧ (𝐺𝑖) ∈ V) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
135132, 133, 134syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
1361353adant1 1125 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝑖𝑌 ↦ (𝐺𝑖)))
137106eqcomd 2767 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑖𝑌 ↦ (𝐺𝑖)) = ran (𝐺𝑌))
1381373ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → ran (𝑖𝑌 ↦ (𝐺𝑖)) = ran (𝐺𝑌))
139136, 138eleqtrd 2842 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋 ∧ (𝐺𝑖) ≠ ∅) → (𝐺𝑖) ∈ ran (𝐺𝑌))
140125, 126, 131, 139syl3anc 1477 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → (𝐺𝑖) ∈ ran (𝐺𝑌))
141124, 140eqeltrd 2840 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ≠ ∅) ∧ 𝑖𝑋 ∧ (𝐺𝑖) = 𝑥) → 𝑥 ∈ ran (𝐺𝑌))
1421413exp 1113 . . . . . . . . . . . . . 14 ((𝜑𝑥 ≠ ∅) → (𝑖𝑋 → ((𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌))))
143142rexlimdv 3169 . . . . . . . . . . . . 13 ((𝜑𝑥 ≠ ∅) → (∃𝑖𝑋 (𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌)))
1441433adant2 1126 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → (∃𝑖𝑋 (𝐺𝑖) = 𝑥𝑥 ∈ ran (𝐺𝑌)))
145121, 144mpd 15 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ran 𝐺𝑥 ≠ ∅) → 𝑥 ∈ ran (𝐺𝑌))
146111, 113, 115, 145syl3anc 1477 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ran 𝐺 ∖ {∅})) → 𝑥 ∈ ran (𝐺𝑌))
147146ralrimiva 3105 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (ran 𝐺 ∖ {∅})𝑥 ∈ ran (𝐺𝑌))
148 dfss3 3734 . . . . . . . . 9 ((ran 𝐺 ∖ {∅}) ⊆ ran (𝐺𝑌) ↔ ∀𝑥 ∈ (ran 𝐺 ∖ {∅})𝑥 ∈ ran (𝐺𝑌))
149147, 148sylibr 224 . . . . . . . 8 (𝜑 → (ran 𝐺 ∖ {∅}) ⊆ ran (𝐺𝑌))
150110, 149eqssd 3762 . . . . . . 7 (𝜑 → ran (𝐺𝑌) = (ran 𝐺 ∖ {∅}))
151105, 150jca 555 . . . . . 6 (𝜑 → ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ∧ ran (𝐺𝑌) = (ran 𝐺 ∖ {∅})))
152 dff1o5 6309 . . . . . 6 ((𝐺𝑌):𝑌1-1-onto→(ran 𝐺 ∖ {∅}) ↔ ((𝐺𝑌):𝑌1-1→(ran 𝐺 ∖ {∅}) ∧ ran (𝐺𝑌) = (ran 𝐺 ∖ {∅})))
153151, 152sylibr 224 . . . . 5 (𝜑 → (𝐺𝑌):𝑌1-1-onto→(ran 𝐺 ∖ {∅}))
154 fvres 6370 . . . . . 6 (𝑗𝑌 → ((𝐺𝑌)‘𝑗) = (𝐺𝑗))
155154adantl 473 . . . . 5 ((𝜑𝑗𝑌) → ((𝐺𝑌)‘𝑗) = (𝐺𝑗))
1561, 45, 42, 80, 153, 155, 18sge0f1o 41121 . . . 4 (𝜑 → (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))) = (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))))
157156eqcomd 2767 . . 3 (𝜑 → (Σ^‘(𝑗𝑌 ↦ (𝑀‘(𝐺𝑗)))) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
15844, 79, 1573eqtrd 2799 . 2 (𝜑 → (Σ^‘(𝑀𝐺)) = (Σ^‘(𝑘 ∈ (ran 𝐺 ∖ {∅}) ↦ (𝑀𝑘))))
15936, 38, 1583eqtr4d 2805 1 (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2140  wne 2933  wral 3051  wrex 3052  {crab 3055  Vcvv 3341  cdif 3713  cin 3715  wss 3716  c0 4059  {csn 4322  Disj wdisj 4773  cmpt 4882  dom cdm 5267  ran crn 5268  cres 5269  ccom 5271   Fn wfn 6045  wf 6046  1-1wf1 6047  1-1-ontowf1o 6049  cfv 6050  (class class class)co 6815  0cc0 10149  +∞cpnf 10284  [,]cicc 12392  Σ^csumge0 41101  Meascmea 41188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-inf2 8714  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225  ax-pre-mulgt0 10226  ax-pre-sup 10227
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-disj 4774  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-se 5227  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-isom 6059  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-om 7233  df-1st 7335  df-2nd 7336  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-oadd 7735  df-er 7914  df-en 8125  df-dom 8126  df-sdom 8127  df-fin 8128  df-sup 8516  df-oi 8583  df-card 8976  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292  df-le 10293  df-sub 10481  df-neg 10482  df-div 10898  df-nn 11234  df-2 11292  df-3 11293  df-n0 11506  df-z 11591  df-uz 11901  df-rp 12047  df-xadd 12161  df-ico 12395  df-icc 12396  df-fz 12541  df-fzo 12681  df-seq 13017  df-exp 13076  df-hash 13333  df-cj 14059  df-re 14060  df-im 14061  df-sqrt 14195  df-abs 14196  df-clim 14439  df-sum 14637  df-sumge0 41102  df-mea 41189
This theorem is referenced by:  meadjiun  41205
  Copyright terms: Public domain W3C validator