| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iccssxr 13471 | . . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* | 
| 2 |  | meadjun.m | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ Meas) | 
| 3 |  | meadjun.x | . . . . . . . . 9
⊢ 𝑆 = dom 𝑀 | 
| 4 | 2, 3 | meaf 46473 | . . . . . . . 8
⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) | 
| 5 |  | meadjun.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑆) | 
| 6 | 4, 5 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → (𝑀‘𝐵) ∈ (0[,]+∞)) | 
| 7 | 1, 6 | sselid 3980 | . . . . . 6
⊢ (𝜑 → (𝑀‘𝐵) ∈
ℝ*) | 
| 8 |  | xaddlid 13285 | . . . . . 6
⊢ ((𝑀‘𝐵) ∈ ℝ* → (0
+𝑒 (𝑀‘𝐵)) = (𝑀‘𝐵)) | 
| 9 | 7, 8 | syl 17 | . . . . 5
⊢ (𝜑 → (0 +𝑒
(𝑀‘𝐵)) = (𝑀‘𝐵)) | 
| 10 | 9 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (𝑀‘𝐵) = (0 +𝑒 (𝑀‘𝐵))) | 
| 11 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘𝐵) = (0 +𝑒 (𝑀‘𝐵))) | 
| 12 |  | uneq1 4160 | . . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = (∅ ∪ 𝐵)) | 
| 13 |  | 0un 4395 | . . . . . . 7
⊢ (∅
∪ 𝐵) = 𝐵 | 
| 14 | 13 | a1i 11 | . . . . . 6
⊢ (𝐴 = ∅ → (∅ ∪
𝐵) = 𝐵) | 
| 15 | 12, 14 | eqtrd 2776 | . . . . 5
⊢ (𝐴 = ∅ → (𝐴 ∪ 𝐵) = 𝐵) | 
| 16 | 15 | fveq2d 6909 | . . . 4
⊢ (𝐴 = ∅ → (𝑀‘(𝐴 ∪ 𝐵)) = (𝑀‘𝐵)) | 
| 17 | 16 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = (𝑀‘𝐵)) | 
| 18 |  | fveq2 6905 | . . . . . 6
⊢ (𝐴 = ∅ → (𝑀‘𝐴) = (𝑀‘∅)) | 
| 19 | 18 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘𝐴) = (𝑀‘∅)) | 
| 20 | 2 | mea0 46474 | . . . . . 6
⊢ (𝜑 → (𝑀‘∅) = 0) | 
| 21 | 20 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘∅) = 0) | 
| 22 | 19, 21 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘𝐴) = 0) | 
| 23 | 22 | oveq1d 7447 | . . 3
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)) = (0 +𝑒 (𝑀‘𝐵))) | 
| 24 | 11, 17, 23 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 25 |  | simpl 482 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝜑) | 
| 26 |  | meadjun.dj | . . . . . 6
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) | 
| 27 | 26 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = ∅) | 
| 28 |  | inidm 4226 | . . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 29 | 28 | eqcomi 2745 | . . . . . . . . . 10
⊢ 𝐴 = (𝐴 ∩ 𝐴) | 
| 30 |  | ineq2 4213 | . . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐴) = (𝐴 ∩ 𝐵)) | 
| 31 | 29, 30 | eqtr2id 2789 | . . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐵) = 𝐴) | 
| 32 | 31 | adantl 481 | . . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) = 𝐴) | 
| 33 |  | neqne 2947 | . . . . . . . . 9
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 = 𝐵) → 𝐴 ≠ ∅) | 
| 35 | 32, 34 | eqnetrd 3007 | . . . . . . 7
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 = 𝐵) → (𝐴 ∩ 𝐵) ≠ ∅) | 
| 36 | 35 | neneqd 2944 | . . . . . 6
⊢ ((¬
𝐴 = ∅ ∧ 𝐴 = 𝐵) → ¬ (𝐴 ∩ 𝐵) = ∅) | 
| 37 | 36 | adantll 714 | . . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 = ∅) ∧ 𝐴 = 𝐵) → ¬ (𝐴 ∩ 𝐵) = ∅) | 
| 38 | 27, 37 | pm2.65da 816 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ¬ 𝐴 = 𝐵) | 
| 39 | 38 | neqned 2946 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝐴 ≠ 𝐵) | 
| 40 |  | meadjun.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑆) | 
| 41 |  | uniprg 4922 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)) | 
| 42 | 40, 5, 41 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) | 
| 43 | 42 | eqcomd 2742 | . . . . . 6
⊢ (𝜑 → (𝐴 ∪ 𝐵) = ∪ {𝐴, 𝐵}) | 
| 44 | 43 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = (𝑀‘∪ {𝐴, 𝐵})) | 
| 45 | 44 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘(𝐴 ∪ 𝐵)) = (𝑀‘∪ {𝐴, 𝐵})) | 
| 46 | 40, 5 | prssd 4821 | . . . . . 6
⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝑆) | 
| 47 |  | prfi 9364 | . . . . . . . 8
⊢ {𝐴, 𝐵} ∈ Fin | 
| 48 |  | isfinite 9693 | . . . . . . . . . 10
⊢ ({𝐴, 𝐵} ∈ Fin ↔ {𝐴, 𝐵} ≺ ω) | 
| 49 | 48 | biimpi 216 | . . . . . . . . 9
⊢ ({𝐴, 𝐵} ∈ Fin → {𝐴, 𝐵} ≺ ω) | 
| 50 |  | sdomdom 9021 | . . . . . . . . 9
⊢ ({𝐴, 𝐵} ≺ ω → {𝐴, 𝐵} ≼ ω) | 
| 51 | 49, 50 | syl 17 | . . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ Fin → {𝐴, 𝐵} ≼ ω) | 
| 52 | 47, 51 | ax-mp 5 | . . . . . . 7
⊢ {𝐴, 𝐵} ≼ ω | 
| 53 | 52 | a1i 11 | . . . . . 6
⊢ (𝜑 → {𝐴, 𝐵} ≼ ω) | 
| 54 |  | disjxsn 5136 | . . . . . . . . . 10
⊢
Disj 𝑥 ∈
{𝐵}𝑥 | 
| 55 | 54 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 = 𝐵 → Disj 𝑥 ∈ {𝐵}𝑥) | 
| 56 |  | preq1 4732 | . . . . . . . . . . 11
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐵, 𝐵}) | 
| 57 |  | dfsn2 4638 | . . . . . . . . . . . . 13
⊢ {𝐵} = {𝐵, 𝐵} | 
| 58 | 57 | eqcomi 2745 | . . . . . . . . . . . 12
⊢ {𝐵, 𝐵} = {𝐵} | 
| 59 | 58 | a1i 11 | . . . . . . . . . . 11
⊢ (𝐴 = 𝐵 → {𝐵, 𝐵} = {𝐵}) | 
| 60 | 56, 59 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐵}) | 
| 61 | 60 | disjeq1d 5117 | . . . . . . . . 9
⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ {𝐴, 𝐵}𝑥 ↔ Disj 𝑥 ∈ {𝐵}𝑥)) | 
| 62 | 55, 61 | mpbird 257 | . . . . . . . 8
⊢ (𝐴 = 𝐵 → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥) | 
| 63 | 62 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥) | 
| 64 |  | simpl 482 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 𝐵) → 𝜑) | 
| 65 |  | neqne 2947 | . . . . . . . . 9
⊢ (¬
𝐴 = 𝐵 → 𝐴 ≠ 𝐵) | 
| 66 | 65 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 𝐵) → 𝐴 ≠ 𝐵) | 
| 67 | 26 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 ∩ 𝐵) = ∅) | 
| 68 | 40 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑆) | 
| 69 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑆) | 
| 70 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) | 
| 71 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 72 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) | 
| 73 | 71, 72 | disjprg 5138 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝑥 ↔ (𝐴 ∩ 𝐵) = ∅)) | 
| 74 | 68, 69, 70, 73 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝑥 ↔ (𝐴 ∩ 𝐵) = ∅)) | 
| 75 | 67, 74 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥) | 
| 76 | 64, 66, 75 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = 𝐵) → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥) | 
| 77 | 63, 76 | pm2.61dan 812 | . . . . . 6
⊢ (𝜑 → Disj 𝑥 ∈ {𝐴, 𝐵}𝑥) | 
| 78 | 2, 3, 46, 53, 77 | meadjuni 46477 | . . . . 5
⊢ (𝜑 → (𝑀‘∪ {𝐴, 𝐵}) =
(Σ^‘(𝑀 ↾ {𝐴, 𝐵}))) | 
| 79 | 78 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘∪ {𝐴, 𝐵}) =
(Σ^‘(𝑀 ↾ {𝐴, 𝐵}))) | 
| 80 | 4, 40 | ffvelcdmd 7104 | . . . . . . 7
⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞)) | 
| 81 | 80 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘𝐴) ∈ (0[,]+∞)) | 
| 82 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘𝐵) ∈ (0[,]+∞)) | 
| 83 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝑀‘𝑥) = (𝑀‘𝐴)) | 
| 84 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝐵 → (𝑀‘𝑥) = (𝑀‘𝐵)) | 
| 85 | 68, 69, 81, 82, 83, 84, 70 | sge0pr 46414 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) →
(Σ^‘(𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥))) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 86 | 4, 46 | fssresd 6774 | . . . . . . . . 9
⊢ (𝜑 → (𝑀 ↾ {𝐴, 𝐵}):{𝐴, 𝐵}⟶(0[,]+∞)) | 
| 87 | 86 | feqmptd 6976 | . . . . . . . 8
⊢ (𝜑 → (𝑀 ↾ {𝐴, 𝐵}) = (𝑥 ∈ {𝐴, 𝐵} ↦ ((𝑀 ↾ {𝐴, 𝐵})‘𝑥))) | 
| 88 |  | fvres 6924 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴, 𝐵} → ((𝑀 ↾ {𝐴, 𝐵})‘𝑥) = (𝑀‘𝑥)) | 
| 89 | 88 | mpteq2ia 5244 | . . . . . . . . 9
⊢ (𝑥 ∈ {𝐴, 𝐵} ↦ ((𝑀 ↾ {𝐴, 𝐵})‘𝑥)) = (𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥)) | 
| 90 | 89 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ {𝐴, 𝐵} ↦ ((𝑀 ↾ {𝐴, 𝐵})‘𝑥)) = (𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥))) | 
| 91 | 87, 90 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (𝑀 ↾ {𝐴, 𝐵}) = (𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥))) | 
| 92 | 91 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑀 ↾ {𝐴, 𝐵})) =
(Σ^‘(𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥)))) | 
| 93 | 92 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) →
(Σ^‘(𝑀 ↾ {𝐴, 𝐵})) =
(Σ^‘(𝑥 ∈ {𝐴, 𝐵} ↦ (𝑀‘𝑥)))) | 
| 94 |  | eqidd 2737 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 95 | 85, 93, 94 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) →
(Σ^‘(𝑀 ↾ {𝐴, 𝐵})) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 96 | 45, 79, 95 | 3eqtrd 2780 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 97 | 25, 39, 96 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | 
| 98 | 24, 97 | pm2.61dan 812 | 1
⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) |