Proof of Theorem caragenuncllem
| Step | Hyp | Ref
| Expression |
| 1 | | caragenuncllem.o |
. . . . . 6
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
| 2 | | caragenuncllem.s |
. . . . . 6
⊢ 𝑆 = (CaraGen‘𝑂) |
| 3 | | caragenuncllem.x |
. . . . . 6
⊢ 𝑋 = ∪
dom 𝑂 |
| 4 | | caragenuncllem.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
| 5 | | caragenuncllem.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
| 6 | 5 | ssinss1d 4247 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ (𝐸 ∪ 𝐹)) ⊆ 𝑋) |
| 7 | 1, 2, 3, 4, 6 | caragensplit 46515 |
. . . . 5
⊢ (𝜑 → ((𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸))) = (𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹)))) |
| 8 | 7 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) = ((𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸)))) |
| 9 | | inass 4228 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸) = (𝐴 ∩ ((𝐸 ∪ 𝐹) ∩ 𝐸)) |
| 10 | | incom 4209 |
. . . . . . . . . 10
⊢ ((𝐸 ∪ 𝐹) ∩ 𝐸) = (𝐸 ∩ (𝐸 ∪ 𝐹)) |
| 11 | | inabs 4266 |
. . . . . . . . . 10
⊢ (𝐸 ∩ (𝐸 ∪ 𝐹)) = 𝐸 |
| 12 | 10, 11 | eqtri 2765 |
. . . . . . . . 9
⊢ ((𝐸 ∪ 𝐹) ∩ 𝐸) = 𝐸 |
| 13 | 12 | ineq2i 4217 |
. . . . . . . 8
⊢ (𝐴 ∩ ((𝐸 ∪ 𝐹) ∩ 𝐸)) = (𝐴 ∩ 𝐸) |
| 14 | 9, 13 | eqtri 2765 |
. . . . . . 7
⊢ ((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸) = (𝐴 ∩ 𝐸) |
| 15 | 14 | fveq2i 6909 |
. . . . . 6
⊢ (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸)) = (𝑂‘(𝐴 ∩ 𝐸)) |
| 16 | | incom 4209 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ 𝐸) ∩ 𝐹) = (𝐹 ∩ (𝐴 ∖ 𝐸)) |
| 17 | | indifcom 4283 |
. . . . . . . . . 10
⊢ (𝐹 ∩ (𝐴 ∖ 𝐸)) = (𝐴 ∩ (𝐹 ∖ 𝐸)) |
| 18 | 16, 17 | eqtr2i 2766 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐹 ∖ 𝐸)) = ((𝐴 ∖ 𝐸) ∩ 𝐹) |
| 19 | 18 | eqcomi 2746 |
. . . . . . . 8
⊢ ((𝐴 ∖ 𝐸) ∩ 𝐹) = (𝐴 ∩ (𝐹 ∖ 𝐸)) |
| 20 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((𝐸 ∪ 𝐹) ∖ 𝐸) = ((𝐸 ∖ 𝐸) ∪ (𝐹 ∖ 𝐸)) |
| 21 | | difid 4376 |
. . . . . . . . . . 11
⊢ (𝐸 ∖ 𝐸) = ∅ |
| 22 | 21 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ((𝐸 ∖ 𝐸) ∪ (𝐹 ∖ 𝐸)) = (∅ ∪ (𝐹 ∖ 𝐸)) |
| 23 | | 0un 4396 |
. . . . . . . . . 10
⊢ (∅
∪ (𝐹 ∖ 𝐸)) = (𝐹 ∖ 𝐸) |
| 24 | 20, 22, 23 | 3eqtrri 2770 |
. . . . . . . . 9
⊢ (𝐹 ∖ 𝐸) = ((𝐸 ∪ 𝐹) ∖ 𝐸) |
| 25 | 24 | ineq2i 4217 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐹 ∖ 𝐸)) = (𝐴 ∩ ((𝐸 ∪ 𝐹) ∖ 𝐸)) |
| 26 | | indif2 4281 |
. . . . . . . 8
⊢ (𝐴 ∩ ((𝐸 ∪ 𝐹) ∖ 𝐸)) = ((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸) |
| 27 | 19, 25, 26 | 3eqtrri 2770 |
. . . . . . 7
⊢ ((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸) = ((𝐴 ∖ 𝐸) ∩ 𝐹) |
| 28 | 27 | fveq2i 6909 |
. . . . . 6
⊢ (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸)) = (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) |
| 29 | 15, 28 | oveq12i 7443 |
. . . . 5
⊢ ((𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹))) |
| 30 | 29 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∩ (𝐸 ∪ 𝐹)) ∖ 𝐸))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)))) |
| 31 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)))) |
| 32 | 8, 30, 31 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)))) |
| 33 | | difun1 4299 |
. . . . 5
⊢ (𝐴 ∖ (𝐸 ∪ 𝐹)) = ((𝐴 ∖ 𝐸) ∖ 𝐹) |
| 34 | 33 | fveq2i 6909 |
. . . 4
⊢ (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹))) = (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) |
| 35 | 34 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹))) = (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))) |
| 36 | 32, 35 | oveq12d 7449 |
. 2
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹))) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)))) |
| 37 | 5 | ssinss1d 4247 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐸) ⊆ 𝑋) |
| 38 | 1, 3, 37 | omexrcl 46522 |
. . . 4
⊢ (𝜑 → (𝑂‘(𝐴 ∩ 𝐸)) ∈
ℝ*) |
| 39 | 1, 3, 37 | omecl 46518 |
. . . . 5
⊢ (𝜑 → (𝑂‘(𝐴 ∩ 𝐸)) ∈ (0[,]+∞)) |
| 40 | 39 | xrge0nemnfd 45343 |
. . . 4
⊢ (𝜑 → (𝑂‘(𝐴 ∩ 𝐸)) ≠ -∞) |
| 41 | 38, 40 | jca 511 |
. . 3
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) ∈ ℝ* ∧ (𝑂‘(𝐴 ∩ 𝐸)) ≠ -∞)) |
| 42 | | caragenuncllem.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
| 43 | 1, 2, 42, 3 | caragenelss 46516 |
. . . . . 6
⊢ (𝜑 → 𝐹 ⊆ 𝑋) |
| 44 | 43 | ssinss2d 45065 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∖ 𝐸) ∩ 𝐹) ⊆ 𝑋) |
| 45 | 1, 3, 44 | omexrcl 46522 |
. . . 4
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ∈
ℝ*) |
| 46 | 1, 3, 44 | omecl 46518 |
. . . . 5
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ∈ (0[,]+∞)) |
| 47 | 46 | xrge0nemnfd 45343 |
. . . 4
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ≠ -∞) |
| 48 | 45, 47 | jca 511 |
. . 3
⊢ (𝜑 → ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ∈ ℝ* ∧ (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ≠ -∞)) |
| 49 | 5 | ssdifssd 4147 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∖ 𝐸) ⊆ 𝑋) |
| 50 | 49 | ssdifssd 4147 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∖ 𝐸) ∖ 𝐹) ⊆ 𝑋) |
| 51 | 1, 3, 50 | omexrcl 46522 |
. . . 4
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ∈
ℝ*) |
| 52 | 1, 3, 50 | omecl 46518 |
. . . . 5
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ∈ (0[,]+∞)) |
| 53 | 52 | xrge0nemnfd 45343 |
. . . 4
⊢ (𝜑 → (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ≠ -∞) |
| 54 | 51, 53 | jca 511 |
. . 3
⊢ (𝜑 → ((𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ∈ ℝ* ∧ (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ≠ -∞)) |
| 55 | | xaddass 13291 |
. . 3
⊢ ((((𝑂‘(𝐴 ∩ 𝐸)) ∈ ℝ* ∧ (𝑂‘(𝐴 ∩ 𝐸)) ≠ -∞) ∧ ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ∈ ℝ* ∧ (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) ≠ -∞) ∧ ((𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ∈ ℝ* ∧ (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)) ≠ -∞)) → (((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹))) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))))) |
| 56 | 41, 48, 54, 55 | syl3anc 1373 |
. 2
⊢ (𝜑 → (((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹))) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))))) |
| 57 | 1, 2, 3, 42, 49 | caragensplit 46515 |
. . . 4
⊢ (𝜑 → ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹))) = (𝑂‘(𝐴 ∖ 𝐸))) |
| 58 | 57 | oveq2d 7447 |
. . 3
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)))) = ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸)))) |
| 59 | 1, 2, 3, 4, 5 | caragensplit 46515 |
. . 3
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸))) = (𝑂‘𝐴)) |
| 60 | 58, 59 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 ((𝑂‘((𝐴 ∖ 𝐸) ∩ 𝐹)) +𝑒 (𝑂‘((𝐴 ∖ 𝐸) ∖ 𝐹)))) = (𝑂‘𝐴)) |
| 61 | 36, 56, 60 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (𝑂‘𝐴)) |