pmeasadd - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pmeasadd		Structured version Visualization version GIF version

Theorem pmeasadd 34566

Description: A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020.)

**Hypotheses**
Ref	Expression
caraext.1	⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞))
caraext.2	⊢ (𝜑 → (𝑃‘∅) = 0)
caraext.3	⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ^*𝑦 ∈ 𝑥(𝑃‘𝑦))
pmeassubadd.q	⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}
pmeassubadd.1	⊢ (𝜑 → 𝑅 ∈ 𝑄)
pmeassubadd.2	⊢ (𝜑 → 𝐴 ≼ ω)
pmeassubadd.3	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑅)
pmeasadd.4	⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)

**Assertion**
Ref	Expression
pmeasadd	⊢ (𝜑 → (𝑃‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ^*𝑘 ∈ 𝐴(𝑃‘𝐵))

Distinct variable groups: 𝑥,𝑃,𝑦 𝑥,𝑅,𝑦 𝜑,𝑥,𝑦 𝐴,𝑘,𝑥,𝑦 𝑥,𝐵,𝑦 𝑃,𝑘 𝑅,𝑘 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑠) 𝐴(𝑠) 𝐵(𝑘,𝑠) 𝑃(𝑠) 𝑄(𝑥,𝑦,𝑘,𝑠) 𝑅(𝑠) 𝑂(𝑥,𝑦,𝑘,𝑠)

**Proof of Theorem pmeasadd**
Step	Hyp	Ref	Expression
1		pmeassubadd.3	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑅)
2	1	ralrimiva 3144	. . . 4 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑅)
3		dfiun3g 5933	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑅 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
4	2, 3	syl 17	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
5	4	fveq2d 6856	. 2 ⊢ (𝜑 → (𝑃‘∪ 𝑘 ∈ 𝐴 𝐵) = (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
6		pmeassubadd.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ≼ ω)
7		mptct 10481	. . . . . 6 ⊢ (𝐴 ≼ ω → (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω)
8		rnct 10468	. . . . . 6 ⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω)
9	6, 7, 8	3syl 18	. . . . 5 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω)
10		eqid 2752	. . . . . . 7 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
11	10	rnmptss 7089	. . . . . 6 ⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑅 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅)
12	2, 11	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅)
13		pmeasadd.4	. . . . . 6 ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)
14		disjrnmpt 32723	. . . . . 6 ⊢ (Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)
15	13, 14	syl 17	. . . . 5 ⊢ (𝜑 → Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)
16	9, 12, 15	3jca 1137	. . . 4 ⊢ (𝜑 → (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦))
17	16	ancli 555	. . 3 ⊢ (𝜑 → (𝜑 ∧ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)))
18		ctex 8929	. . . . 5 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
19		mptexg 7190	. . . . 5 ⊢ (𝐴 ∈ V → (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V)
20	6, 18, 19	3syl 18	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V)
21		rnexg 7868	. . . 4 ⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V)
22		breq1 5093	. . . . . . . 8 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → (𝑥 ≼ ω ↔ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω))
23		sseq1 3952	. . . . . . . 8 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → (𝑥 ⊆ 𝑅 ↔ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅))
24		disjeq1 5064	. . . . . . . 8 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → (Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦))
25	22, 23, 24	3anbi123d 1447	. . . . . . 7 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → ((𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦) ↔ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)))
26	25	anbi2d 638	. . . . . 6 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) ↔ (𝜑 ∧ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦))))
27		unieq 4866	. . . . . . . 8 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → ∪ 𝑥 = ∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
28	27	fveq2d 6856	. . . . . . 7 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → (𝑃‘∪ 𝑥) = (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
29		esumeq1 34275	. . . . . . 7 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → Σ^𝑦 ∈ 𝑥(𝑃‘𝑦) = Σ^𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦))
30	28, 29	eqeq12d 2768	. . . . . 6 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → ((𝑃‘∪ 𝑥) = Σ^𝑦 ∈ 𝑥(𝑃‘𝑦) ↔ (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ^𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦)))
31	26, 30	imbi12d 346	. . . . 5 ⊢ (𝑥 = ran (𝑘 ∈ 𝐴 ↦ 𝐵) → (((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ^𝑦 ∈ 𝑥(𝑃‘𝑦)) ↔ ((𝜑 ∧ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)) → (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ^𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦))))
32		caraext.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦)) → (𝑃‘∪ 𝑥) = Σ^*𝑦 ∈ 𝑥(𝑃‘𝑦))
33	31, 32	vtoclg 3512	. . . 4 ⊢ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V → ((𝜑 ∧ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)) → (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ^*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦)))
34	20, 21, 33	3syl 18	. . 3 ⊢ (𝜑 → ((𝜑 ∧ (ran (𝑘 ∈ 𝐴 ↦ 𝐵) ≼ ω ∧ ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)𝑦)) → (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ^*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦)))
35	17, 34	mpd 15	. 2 ⊢ (𝜑 → (𝑃‘∪ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ^*𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦))
36		fveq2 6852	. . 3 ⊢ (𝑦 = 𝐵 → (𝑃‘𝑦) = (𝑃‘𝐵))
37	6, 18	syl 17	. . 3 ⊢ (𝜑 → 𝐴 ∈ V)
38		caraext.1	. . . . 5 ⊢ (𝜑 → 𝑃:𝑅⟶(0[,]+∞))
39	38	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃:𝑅⟶(0[,]+∞))
40	39, 1	ffvelcdmd 7051	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑃‘𝐵) ∈ (0[,]+∞))
41		fveq2 6852	. . . . 5 ⊢ (𝐵 = ∅ → (𝑃‘𝐵) = (𝑃‘∅))
42	41	adantl 484	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → (𝑃‘𝐵) = (𝑃‘∅))
43		caraext.2	. . . . 5 ⊢ (𝜑 → (𝑃‘∅) = 0)
44	43	ad2antrr 734	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → (𝑃‘∅) = 0)
45	42, 44	eqtrd 2787	. . 3 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝐵 = ∅) → (𝑃‘𝐵) = 0)
46	36, 37, 40, 1, 45, 13	esumrnmpt2 34309	. 2 ⊢ (𝜑 → Σ^𝑦 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)(𝑃‘𝑦) = Σ^𝑘 ∈ 𝐴(𝑃‘𝐵))
47	5, 35, 46	3eqtrd 2791	1 ⊢ (𝜑 → (𝑃‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ^*𝑘 ∈ 𝐴(𝑃‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1095 = wceq 1550 ∈ wcel 2132 ∀wral 3066 {crab 3404 Vcvv 3444 ∖ cdif 3892 ∪ cun 3893 ⊆ wss 3895 ∅c0 4276 𝒫 cpw 4545 ∪ cuni 4855 ∪ ciun 4939 Disj wdisj 5057 class class class wbr 5090 ↦ cmpt 5171 ran crn 5637 ⟶wf 6502 ‘cfv 6506 (class class class)co 7381 ωcom 7831 ≼ cdom 8910 0cc0 11059 +∞cpnf 11199 [,]cicc 13338 Σ^*cesum 34268

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703 ax-inf2 9582 ax-ac2 10406 ax-cnex 11115 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 ax-pre-sup 11137 ax-addf 11138 ax-mulf 11139

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-nel 3052 df-ral 3067 df-rex 3077 df-rmo 3357 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4856 df-int 4896 df-iun 4941 df-iin 4942 df-disj 5058 df-br 5091 df-opab 5153 df-mpt 5172 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-se 5590 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-pred 6273 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-isom 6515 df-riota 7338 df-ov 7384 df-oprab 7385 df-mpo 7386 df-of 7645 df-om 7832 df-1st 7955 df-2nd 7956 df-supp 8125 df-frecs 8246 df-wrecs 8277 df-recs 8326 df-rdg 8365 df-1o 8421 df-2o 8422 df-er 8662 df-map 8794 df-pm 8795 df-ixp 8865 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-fsupp 9294 df-fi 9343 df-sup 9374 df-inf 9375 df-oi 9444 df-card 9883 df-acn 9886 df-ac 10058 df-pnf 11204 df-mnf 11205 df-xr 11206 df-ltxr 11207 df-le 11208 df-sub 11402 df-neg 11403 df-div 11831 df-nn 12197 df-2 12266 df-3 12267 df-4 12268 df-5 12269 df-6 12270 df-7 12271 df-8 12272 df-9 12273 df-n0 12468 df-z 12555 df-dec 12675 df-uz 12826 df-q 12936 df-rp 12980 df-xneg 13100 df-xadd 13101 df-xmul 13102 df-ioo 13339 df-ioc 13340 df-ico 13341 df-icc 13342 df-fz 13499 df-fzo 13646 df-fl 13788 df-mod 13866 df-seq 14001 df-exp 14061 df-fac 14273 df-bc 14302 df-hash 14330 df-shft 15066 df-cj 15098 df-re 15099 df-im 15100 df-sqrt 15234 df-abs 15235 df-limsup 15470 df-clim 15487 df-rlim 15488 df-sum 15686 df-ef 16069 df-sin 16071 df-cos 16072 df-pi 16074 df-struct 17155 df-sets 17172 df-slot 17190 df-ndx 17202 df-base 17218 df-ress 17239 df-plusg 17271 df-mulr 17272 df-starv 17273 df-sca 17274 df-vsca 17275 df-ip 17276 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-hom 17282 df-cco 17283 df-rest 17423 df-topn 17424 df-0g 17442 df-gsum 17443 df-topgen 17444 df-pt 17445 df-prds 17448 df-ordt 17503 df-xrs 17504 df-qtop 17509 df-imas 17510 df-xps 17512 df-mre 17586 df-mrc 17587 df-acs 17589 df-ps 18570 df-tsr 18571 df-plusf 18645 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-mhm 18789 df-submnd 18790 df-grp 18950 df-minusg 18951 df-sbg 18952 df-mulg 19082 df-subg 19137 df-cntz 19329 df-cmn 19794 df-abl 19795 df-mgp 20159 df-rng 20171 df-ur 20200 df-ring 20253 df-cring 20254 df-subrng 20564 df-subrg 20588 df-abv 20827 df-lmod 20898 df-scaf 20899 df-sra 21209 df-rgmod 21210 df-psmet 21385 df-xmet 21386 df-met 21387 df-bl 21388 df-mopn 21389 df-fbas 21390 df-fg 21391 df-cnfld 21394 df-top 22923 df-topon 22940 df-topsp 22962 df-bases 22975 df-cld 23048 df-ntr 23049 df-cls 23050 df-nei 23127 df-lp 23165 df-perf 23166 df-cn 23256 df-cnp 23257 df-haus 23344 df-tx 23591 df-hmeo 23784 df-fil 23875 df-fm 23967 df-flim 23968 df-flf 23969 df-tmd 24101 df-tgp 24102 df-tsms 24156 df-trg 24189 df-xms 24349 df-ms 24350 df-tms 24351 df-nm 24611 df-ngp 24612 df-nrg 24614 df-nlm 24615 df-ii 24908 df-cncf 24909 df-limc 25897 df-dv 25898 df-log 26587 df-esum 34269

This theorem is referenced by: (None)

W3C validator