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