# Metamath Proof Explorer

Description: The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjun.m ${⊢}{\phi }\to {M}\in \mathrm{Meas}$
meadjun.x ${⊢}{S}=\mathrm{dom}{M}$
meadjun.a ${⊢}{\phi }\to {A}\in {S}$
meadjun.b ${⊢}{\phi }\to {B}\in {S}$
meadjun.dj ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
Assertion meadjun ${⊢}{\phi }\to {M}\left({A}\cup {B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 meadjun.m ${⊢}{\phi }\to {M}\in \mathrm{Meas}$
2 meadjun.x ${⊢}{S}=\mathrm{dom}{M}$
3 meadjun.a ${⊢}{\phi }\to {A}\in {S}$
4 meadjun.b ${⊢}{\phi }\to {B}\in {S}$
5 meadjun.dj ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
6 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
7 1 2 meaf ${⊢}{\phi }\to {M}:{S}⟶\left[0,\mathrm{+\infty }\right]$
8 7 4 ffvelrnd ${⊢}{\phi }\to {M}\left({B}\right)\in \left[0,\mathrm{+\infty }\right]$
9 6 8 sseldi ${⊢}{\phi }\to {M}\left({B}\right)\in {ℝ}^{*}$
10 xaddid2 ${⊢}{M}\left({B}\right)\in {ℝ}^{*}\to 0{+}_{𝑒}{M}\left({B}\right)={M}\left({B}\right)$
11 9 10 syl ${⊢}{\phi }\to 0{+}_{𝑒}{M}\left({B}\right)={M}\left({B}\right)$
12 11 eqcomd ${⊢}{\phi }\to {M}\left({B}\right)=0{+}_{𝑒}{M}\left({B}\right)$
13 12 adantr ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({B}\right)=0{+}_{𝑒}{M}\left({B}\right)$
14 uneq1 ${⊢}{A}=\varnothing \to {A}\cup {B}=\varnothing \cup {B}$
15 0un ${⊢}\varnothing \cup {B}={B}$
16 15 a1i ${⊢}{A}=\varnothing \to \varnothing \cup {B}={B}$
17 14 16 eqtrd ${⊢}{A}=\varnothing \to {A}\cup {B}={B}$
18 17 fveq2d ${⊢}{A}=\varnothing \to {M}\left({A}\cup {B}\right)={M}\left({B}\right)$
19 18 adantl ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({A}\cup {B}\right)={M}\left({B}\right)$
20 fveq2 ${⊢}{A}=\varnothing \to {M}\left({A}\right)={M}\left(\varnothing \right)$
21 20 adantl ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({A}\right)={M}\left(\varnothing \right)$
22 1 mea0 ${⊢}{\phi }\to {M}\left(\varnothing \right)=0$
23 22 adantr ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left(\varnothing \right)=0$
24 21 23 eqtrd ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({A}\right)=0$
25 24 oveq1d ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)=0{+}_{𝑒}{M}\left({B}\right)$
26 13 19 25 3eqtr4d ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {M}\left({A}\cup {B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
27 simpl ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to {\phi }$
28 5 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{A}=\varnothing \right)\wedge {A}={B}\right)\to {A}\cap {B}=\varnothing$
29 inidm ${⊢}{A}\cap {A}={A}$
30 29 eqcomi ${⊢}{A}={A}\cap {A}$
31 ineq2 ${⊢}{A}={B}\to {A}\cap {A}={A}\cap {B}$
32 30 31 syl5req ${⊢}{A}={B}\to {A}\cap {B}={A}$
33 32 adantl ${⊢}\left(¬{A}=\varnothing \wedge {A}={B}\right)\to {A}\cap {B}={A}$
34 neqne ${⊢}¬{A}=\varnothing \to {A}\ne \varnothing$
35 34 adantr ${⊢}\left(¬{A}=\varnothing \wedge {A}={B}\right)\to {A}\ne \varnothing$
36 33 35 eqnetrd ${⊢}\left(¬{A}=\varnothing \wedge {A}={B}\right)\to {A}\cap {B}\ne \varnothing$
37 36 neneqd ${⊢}\left(¬{A}=\varnothing \wedge {A}={B}\right)\to ¬{A}\cap {B}=\varnothing$
38 37 adantll ${⊢}\left(\left({\phi }\wedge ¬{A}=\varnothing \right)\wedge {A}={B}\right)\to ¬{A}\cap {B}=\varnothing$
39 28 38 pm2.65da ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to ¬{A}={B}$
40 39 neqned ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to {A}\ne {B}$
41 uniprg ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to \bigcup \left\{{A},{B}\right\}={A}\cup {B}$
42 3 4 41 syl2anc ${⊢}{\phi }\to \bigcup \left\{{A},{B}\right\}={A}\cup {B}$
43 42 eqcomd ${⊢}{\phi }\to {A}\cup {B}=\bigcup \left\{{A},{B}\right\}$
44 43 fveq2d ${⊢}{\phi }\to {M}\left({A}\cup {B}\right)={M}\left(\bigcup \left\{{A},{B}\right\}\right)$
45 44 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({A}\cup {B}\right)={M}\left(\bigcup \left\{{A},{B}\right\}\right)$
46 3 4 prssd ${⊢}{\phi }\to \left\{{A},{B}\right\}\subseteq {S}$
47 prfi ${⊢}\left\{{A},{B}\right\}\in \mathrm{Fin}$
48 isfinite ${⊢}\left\{{A},{B}\right\}\in \mathrm{Fin}↔\left\{{A},{B}\right\}\prec \mathrm{\omega }$
49 48 biimpi ${⊢}\left\{{A},{B}\right\}\in \mathrm{Fin}\to \left\{{A},{B}\right\}\prec \mathrm{\omega }$
50 sdomdom ${⊢}\left\{{A},{B}\right\}\prec \mathrm{\omega }\to \left\{{A},{B}\right\}\preccurlyeq \mathrm{\omega }$
51 49 50 syl ${⊢}\left\{{A},{B}\right\}\in \mathrm{Fin}\to \left\{{A},{B}\right\}\preccurlyeq \mathrm{\omega }$
52 47 51 ax-mp ${⊢}\left\{{A},{B}\right\}\preccurlyeq \mathrm{\omega }$
53 52 a1i ${⊢}{\phi }\to \left\{{A},{B}\right\}\preccurlyeq \mathrm{\omega }$
54 disjxsn ${⊢}\underset{{x}\in \left\{{B}\right\}}{Disj}{x}$
55 54 a1i ${⊢}{A}={B}\to \underset{{x}\in \left\{{B}\right\}}{Disj}{x}$
56 preq1 ${⊢}{A}={B}\to \left\{{A},{B}\right\}=\left\{{B},{B}\right\}$
57 dfsn2 ${⊢}\left\{{B}\right\}=\left\{{B},{B}\right\}$
58 57 eqcomi ${⊢}\left\{{B},{B}\right\}=\left\{{B}\right\}$
59 58 a1i ${⊢}{A}={B}\to \left\{{B},{B}\right\}=\left\{{B}\right\}$
60 56 59 eqtrd ${⊢}{A}={B}\to \left\{{A},{B}\right\}=\left\{{B}\right\}$
61 60 disjeq1d ${⊢}{A}={B}\to \left(\underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}↔\underset{{x}\in \left\{{B}\right\}}{Disj}{x}\right)$
62 55 61 mpbird ${⊢}{A}={B}\to \underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}$
63 62 adantl ${⊢}\left({\phi }\wedge {A}={B}\right)\to \underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}$
64 simpl ${⊢}\left({\phi }\wedge ¬{A}={B}\right)\to {\phi }$
65 neqne ${⊢}¬{A}={B}\to {A}\ne {B}$
66 65 adantl ${⊢}\left({\phi }\wedge ¬{A}={B}\right)\to {A}\ne {B}$
67 5 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\cap {B}=\varnothing$
68 3 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\in {S}$
69 4 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {B}\in {S}$
70 simpr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {A}\ne {B}$
71 id ${⊢}{x}={A}\to {x}={A}$
72 id ${⊢}{x}={B}\to {x}={B}$
73 71 72 disjprg ${⊢}\left({A}\in {S}\wedge {B}\in {S}\wedge {A}\ne {B}\right)\to \left(\underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}↔{A}\cap {B}=\varnothing \right)$
74 68 69 70 73 syl3anc ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left(\underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}↔{A}\cap {B}=\varnothing \right)$
75 67 74 mpbird ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}$
76 64 66 75 syl2anc ${⊢}\left({\phi }\wedge ¬{A}={B}\right)\to \underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}$
77 63 76 pm2.61dan ${⊢}{\phi }\to \underset{{x}\in \left\{{A},{B}\right\}}{Disj}{x}$
78 1 2 46 53 77 meadjuni ${⊢}{\phi }\to {M}\left(\bigcup \left\{{A},{B}\right\}\right)=\mathrm{sum^}\left({{M}↾}_{\left\{{A},{B}\right\}}\right)$
79 78 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left(\bigcup \left\{{A},{B}\right\}\right)=\mathrm{sum^}\left({{M}↾}_{\left\{{A},{B}\right\}}\right)$
80 7 3 ffvelrnd ${⊢}{\phi }\to {M}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]$
81 80 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]$
82 8 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({B}\right)\in \left[0,\mathrm{+\infty }\right]$
83 fveq2 ${⊢}{x}={A}\to {M}\left({x}\right)={M}\left({A}\right)$
84 fveq2 ${⊢}{x}={B}\to {M}\left({x}\right)={M}\left({B}\right)$
85 68 69 81 82 83 84 70 sge0pr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \mathrm{sum^}\left(\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
86 7 46 fssresd ${⊢}{\phi }\to \left({{M}↾}_{\left\{{A},{B}\right\}}\right):\left\{{A},{B}\right\}⟶\left[0,\mathrm{+\infty }\right]$
87 86 feqmptd ${⊢}{\phi }\to {{M}↾}_{\left\{{A},{B}\right\}}=\left({x}\in \left\{{A},{B}\right\}⟼\left({{M}↾}_{\left\{{A},{B}\right\}}\right)\left({x}\right)\right)$
88 fvres ${⊢}{x}\in \left\{{A},{B}\right\}\to \left({{M}↾}_{\left\{{A},{B}\right\}}\right)\left({x}\right)={M}\left({x}\right)$
89 88 mpteq2ia ${⊢}\left({x}\in \left\{{A},{B}\right\}⟼\left({{M}↾}_{\left\{{A},{B}\right\}}\right)\left({x}\right)\right)=\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)$
90 89 a1i ${⊢}{\phi }\to \left({x}\in \left\{{A},{B}\right\}⟼\left({{M}↾}_{\left\{{A},{B}\right\}}\right)\left({x}\right)\right)=\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)$
91 87 90 eqtrd ${⊢}{\phi }\to {{M}↾}_{\left\{{A},{B}\right\}}=\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)$
92 91 fveq2d ${⊢}{\phi }\to \mathrm{sum^}\left({{M}↾}_{\left\{{A},{B}\right\}}\right)=\mathrm{sum^}\left(\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)\right)$
93 92 adantr ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \mathrm{sum^}\left({{M}↾}_{\left\{{A},{B}\right\}}\right)=\mathrm{sum^}\left(\left({x}\in \left\{{A},{B}\right\}⟼{M}\left({x}\right)\right)\right)$
94 eqidd ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
95 85 93 94 3eqtr4d ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \mathrm{sum^}\left({{M}↾}_{\left\{{A},{B}\right\}}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
96 45 79 95 3eqtrd ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to {M}\left({A}\cup {B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
97 27 40 96 syl2anc ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to {M}\left({A}\cup {B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$
98 26 97 pm2.61dan ${⊢}{\phi }\to {M}\left({A}\cup {B}\right)={M}\left({A}\right){+}_{𝑒}{M}\left({B}\right)$