Theorem meadjiun

Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meadjiun.1	⊢ Ⅎ 𝑘 𝜑
	meadjiun.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meadjiun.s	⊢ 𝑆 = dom 𝑀
	meadjiun.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
	meadjiun.a	⊢ ( 𝜑 → 𝐴 ≼ ω )
	meadjiun.dj	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
Assertion	meadjiun	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		meadjiun.1	⊢ Ⅎ 𝑘 𝜑
2		meadjiun.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
3		meadjiun.s	⊢ 𝑆 = dom 𝑀
4		meadjiun.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
5		meadjiun.a	⊢ ( 𝜑 → 𝐴 ≼ ω )
6		meadjiun.dj	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
7	4	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐵 ∈ 𝑆 ) )
8	1 7	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )
9		dfiun3g	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
10	8 9	syl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
11	10	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
12		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
13	1 12 4	rnmptssd	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑆 )
14		1stcrestlem	⊢ ( 𝐴 ≼ ω → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
15	5 14	syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
16	12	disjrnmpt2	⊢ ( Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑥 )
17	6 16	syl	⊢ ( 𝜑 → Disj 𝑥 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑥 )
18	2 3 13 15 17	meadjuni	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) )
19		reldom	⊢ Rel ≼
20		brrelex1	⊢ ( ( Rel ≼ ∧ 𝐴 ≼ ω ) → 𝐴 ∈ V )
21	19 20	mpan	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
22	5 21	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
23	1 4 12	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑆 )
24		fveq2	⊢ ( 𝑗 = 𝑖 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) )
25	24	neeq1d	⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) ≠ ∅ ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) ≠ ∅ ) )
26	25	cbvrabv	⊢ { 𝑗 ∈ 𝐴 ∣ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) ≠ ∅ } = { 𝑖 ∈ 𝐴 ∣ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) ≠ ∅ }
27		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
28		nfv	⊢ Ⅎ 𝑘 𝑖 ∈ 𝐴
29	1 28	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝐴 )
30		nfcv	⊢ Ⅎ 𝑘 𝑖
31	30	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
32		nfcv	⊢ Ⅎ 𝑘 𝑆
33	31 32	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆
34	29 33	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 )
35		eleq1w	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
36	35	anbi2d	⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) )
37		csbeq1a	⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
38	37	eleq1d	⊢ ( 𝑘 = 𝑖 → ( 𝐵 ∈ 𝑆 ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 ) )
39	36 38	imbi12d	⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 ) ) )
40	34 39 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 )
41	30 31 37 12	fvmptf	⊢ ( ( 𝑖 ∈ 𝐴 ∧ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ 𝑆 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
42	27 40 41	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
43	42	disjeq2dv	⊢ ( 𝜑 → ( Disj 𝑖 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) ↔ Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
44		nfcv	⊢ Ⅎ 𝑖 𝐵
45	44 31 37	cbvdisj	⊢ ( Disj 𝑘 ∈ 𝐴 𝐵 ↔ Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
46	45	bicomi	⊢ ( Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ↔ Disj 𝑘 ∈ 𝐴 𝐵 )
47	46	a1i	⊢ ( 𝜑 → ( Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ↔ Disj 𝑘 ∈ 𝐴 𝐵 ) )
48	43 47	bitrd	⊢ ( 𝜑 → ( Disj 𝑖 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) ↔ Disj 𝑘 ∈ 𝐴 𝐵 ) )
49	6 48	mpbird	⊢ ( 𝜑 → Disj 𝑖 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑖 ) )
50	2 3 22 23 26 49	meadjiunlem	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) = ( Σ^ ‘ ( 𝑀 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) )
51	44 31 37	cbvmpt	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
52	51	coeq2i	⊢ ( 𝑀 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑀 ∘ ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
53	52	a1i	⊢ ( 𝜑 → ( 𝑀 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑀 ∘ ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) ) )
54		eqidd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
55	2 3	meaf	⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
56	55	feqmptd	⊢ ( 𝜑 → 𝑀 = ( 𝑦 ∈ 𝑆 ↦ ( 𝑀 ‘ 𝑦 ) ) )
57		fveq2	⊢ ( 𝑦 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
58	40 54 56 57	fmptco	⊢ ( 𝜑 → ( 𝑀 ∘ ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) ) )
59		nfcv	⊢ Ⅎ 𝑖 ( 𝑀 ‘ 𝐵 )
60		nfcv	⊢ Ⅎ 𝑘 𝑀
61	60 31	nffv	⊢ Ⅎ 𝑘 ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
62	37	fveq2d	⊢ ( 𝑘 = 𝑖 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
63	59 61 62	cbvmpt	⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) )
64	63	eqcomi	⊢ ( 𝑖 ∈ 𝐴 ↦ ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) )
65	64	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐴 ↦ ( 𝑀 ‘ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) )
66	53 58 65	3eqtrd	⊢ ( 𝜑 → ( 𝑀 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) )
67	66	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑀 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) ) )
68	50 67	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑀 ↾ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) ) )
69	11 18 68	3eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ ( 𝑀 ‘ 𝐵 ) ) ) )