| Step | Hyp | Ref
| Expression |
| 1 | | difssd 4137 |
. . 3
⊢ (𝜑 → (𝑂 ∖ 𝐴) ⊆ 𝑂) |
| 2 | | indif2 4281 |
. . . . . . . 8
⊢ (𝑒 ∩ (𝑂 ∖ 𝐴)) = ((𝑒 ∩ 𝑂) ∖ 𝐴) |
| 3 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ 𝒫 𝑂 → 𝑒 ⊆ 𝑂) |
| 4 | 3 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑒 ⊆ 𝑂) |
| 5 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (𝑒 ⊆ 𝑂 ↔ (𝑒 ∩ 𝑂) = 𝑒) |
| 6 | 4, 5 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ 𝑂) = 𝑒) |
| 7 | 6 | difeq1d 4125 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑒 ∩ 𝑂) ∖ 𝐴) = (𝑒 ∖ 𝐴)) |
| 8 | 2, 7 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ (𝑂 ∖ 𝐴)) = (𝑒 ∖ 𝐴)) |
| 9 | 8 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) = (𝑀‘(𝑒 ∖ 𝐴))) |
| 10 | | difdif2 4296 |
. . . . . . . 8
⊢ (𝑒 ∖ (𝑂 ∖ 𝐴)) = ((𝑒 ∖ 𝑂) ∪ (𝑒 ∩ 𝐴)) |
| 11 | | ssdif0 4366 |
. . . . . . . . . . 11
⊢ (𝑒 ⊆ 𝑂 ↔ (𝑒 ∖ 𝑂) = ∅) |
| 12 | 4, 11 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ 𝑂) = ∅) |
| 13 | 12 | uneq1d 4167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑒 ∖ 𝑂) ∪ (𝑒 ∩ 𝐴)) = (∅ ∪ (𝑒 ∩ 𝐴))) |
| 14 | | uncom 4158 |
. . . . . . . . . 10
⊢ ((𝑒 ∩ 𝐴) ∪ ∅) = (∅ ∪ (𝑒 ∩ 𝐴)) |
| 15 | | un0 4394 |
. . . . . . . . . 10
⊢ ((𝑒 ∩ 𝐴) ∪ ∅) = (𝑒 ∩ 𝐴) |
| 16 | 14, 15 | eqtr3i 2767 |
. . . . . . . . 9
⊢ (∅
∪ (𝑒 ∩ 𝐴)) = (𝑒 ∩ 𝐴) |
| 17 | 13, 16 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑒 ∖ 𝑂) ∪ (𝑒 ∩ 𝐴)) = (𝑒 ∩ 𝐴)) |
| 18 | 10, 17 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ (𝑂 ∖ 𝐴)) = (𝑒 ∩ 𝐴)) |
| 19 | 18 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴))) = (𝑀‘(𝑒 ∩ 𝐴))) |
| 20 | 9, 19 | oveq12d 7449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) +𝑒 (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴)))) = ((𝑀‘(𝑒 ∖ 𝐴)) +𝑒 (𝑀‘(𝑒 ∩ 𝐴)))) |
| 21 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
| 22 | | carsgval.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 24 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑒 ∈ 𝒫 𝑂) |
| 25 | 24 | elpwdifcl 32545 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ 𝐴) ∈ 𝒫 𝑂) |
| 26 | 23, 25 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ 𝐴)) ∈ (0[,]+∞)) |
| 27 | 21, 26 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ 𝐴)) ∈
ℝ*) |
| 28 | 24 | elpwincl1 32544 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ 𝐴) ∈ 𝒫 𝑂) |
| 29 | 23, 28 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 30 | 21, 29 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ 𝐴)) ∈
ℝ*) |
| 31 | | xaddcom 13282 |
. . . . . 6
⊢ (((𝑀‘(𝑒 ∖ 𝐴)) ∈ ℝ* ∧ (𝑀‘(𝑒 ∩ 𝐴)) ∈ ℝ*) →
((𝑀‘(𝑒 ∖ 𝐴)) +𝑒 (𝑀‘(𝑒 ∩ 𝐴))) = ((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴)))) |
| 32 | 27, 30, 31 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∖ 𝐴)) +𝑒 (𝑀‘(𝑒 ∩ 𝐴))) = ((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴)))) |
| 33 | | difelcarsg.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀)) |
| 34 | | carsgval.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 35 | 34, 22 | elcarsg 34307 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)))) |
| 36 | 33, 35 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))) |
| 37 | 36 | simprd 495 |
. . . . . 6
⊢ (𝜑 → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)) |
| 38 | 37 | r19.21bi 3251 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)) |
| 39 | 20, 32, 38 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) +𝑒 (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴)))) = (𝑀‘𝑒)) |
| 40 | 39 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) +𝑒 (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴)))) = (𝑀‘𝑒)) |
| 41 | 1, 40 | jca 511 |
. 2
⊢ (𝜑 → ((𝑂 ∖ 𝐴) ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) +𝑒 (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴)))) = (𝑀‘𝑒))) |
| 42 | 34, 22 | elcarsg 34307 |
. 2
⊢ (𝜑 → ((𝑂 ∖ 𝐴) ∈ (toCaraSiga‘𝑀) ↔ ((𝑂 ∖ 𝐴) ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ (𝑂 ∖ 𝐴))) +𝑒 (𝑀‘(𝑒 ∖ (𝑂 ∖ 𝐴)))) = (𝑀‘𝑒)))) |
| 43 | 41, 42 | mpbird 257 |
1
⊢ (𝜑 → (𝑂 ∖ 𝐴) ∈ (toCaraSiga‘𝑀)) |