Proof of Theorem dvle
Step | Hyp | Ref
| Expression |
1 | | dvle.r |
. . . 4
⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅) |
2 | 1 | eleq1d 2891 |
. . 3
⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ 𝑅 ∈ ℝ)) |
3 | | dvle.a |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
4 | | cncff 23066 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
6 | | eqid 2825 |
. . . . 5
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
7 | 6 | fmpt 6629 |
. . . 4
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
8 | 5, 7 | sylibr 226 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) |
9 | | dvle.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁)) |
10 | 2, 8, 9 | rspcdva 3532 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
11 | | dvle.s |
. . . . 5
⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆) |
12 | 11 | eleq1d 2891 |
. . . 4
⊢ (𝑥 = 𝑌 → (𝐶 ∈ ℝ ↔ 𝑆 ∈ ℝ)) |
13 | | dvle.c |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
14 | | cncff 23066 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
16 | | eqid 2825 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) |
17 | 16 | fmpt 6629 |
. . . . 5
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐶 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
18 | 15, 17 | sylibr 226 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐶 ∈ ℝ) |
19 | 12, 18, 9 | rspcdva 3532 |
. . 3
⊢ (𝜑 → 𝑆 ∈ ℝ) |
20 | | dvle.q |
. . . . 5
⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄) |
21 | 20 | eleq1d 2891 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐶 ∈ ℝ ↔ 𝑄 ∈ ℝ)) |
22 | | dvle.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁)) |
23 | 21, 18, 22 | rspcdva 3532 |
. . 3
⊢ (𝜑 → 𝑄 ∈ ℝ) |
24 | 19, 23 | resubcld 10782 |
. 2
⊢ (𝜑 → (𝑆 − 𝑄) ∈ ℝ) |
25 | | dvle.p |
. . . 4
⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃) |
26 | 25 | eleq1d 2891 |
. . 3
⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ 𝑃 ∈ ℝ)) |
27 | 26, 8, 22 | rspcdva 3532 |
. 2
⊢ (𝜑 → 𝑃 ∈ ℝ) |
28 | 10 | recnd 10385 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℂ) |
29 | 23 | recnd 10385 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℂ) |
30 | 19 | recnd 10385 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
31 | 29, 30 | subcld 10713 |
. . . . 5
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℂ) |
32 | 28, 31 | addcomd 10557 |
. . . 4
⊢ (𝜑 → (𝑅 + (𝑄 − 𝑆)) = ((𝑄 − 𝑆) + 𝑅)) |
33 | 28, 30, 29 | subsub2d 10742 |
. . . 4
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) = (𝑅 + (𝑄 − 𝑆))) |
34 | 29, 30, 28 | subsubd 10741 |
. . . 4
⊢ (𝜑 → (𝑄 − (𝑆 − 𝑅)) = ((𝑄 − 𝑆) + 𝑅)) |
35 | 32, 33, 34 | 3eqtr4d 2871 |
. . 3
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) = (𝑄 − (𝑆 − 𝑅))) |
36 | 19, 10 | resubcld 10782 |
. . . 4
⊢ (𝜑 → (𝑆 − 𝑅) ∈ ℝ) |
37 | | dvle.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
38 | | dvle.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
39 | | eqid 2825 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
40 | 39 | subcn 23039 |
. . . . . . 7
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
41 | | ax-resscn 10309 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
42 | | resubcl 10666 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
43 | 39, 40, 13, 3, 41, 42 | cncfmpt2ss 23088 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
44 | | ioossicc 12547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
45 | 44 | sseli 3823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
46 | 18 | r19.21bi 3141 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℝ) |
47 | 45, 46 | sylan2 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℝ) |
48 | 47 | fmpttd 6634 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℝ) |
49 | | ioossre 12523 |
. . . . . . . . . . . . . 14
⊢ (𝑀(,)𝑁) ⊆ ℝ |
50 | | dvfre 24113 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ) |
51 | 48, 49, 50 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ) |
52 | | dvle.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) |
53 | 52 | dmeqd 5558 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) |
54 | | dvle.f |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷) |
55 | | lerel 10421 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
≤ |
56 | 55 | brrelex2i 5394 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ≤ 𝐷 → 𝐷 ∈ V) |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐷 ∈ V) |
58 | 57 | ralrimiva 3175 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐷 ∈ V) |
59 | | dmmptg 5873 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐷 ∈ V → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) = (𝑀(,)𝑁)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) = (𝑀(,)𝑁)) |
61 | 53, 60 | eqtrd 2861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑀(,)𝑁)) |
62 | 52, 61 | feq12d 6266 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷):(𝑀(,)𝑁)⟶ℝ)) |
63 | 51, 62 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷):(𝑀(,)𝑁)⟶ℝ) |
64 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) |
65 | 64 | fmpt 6629 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐷 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷):(𝑀(,)𝑁)⟶ℝ) |
66 | 63, 65 | sylibr 226 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐷 ∈ ℝ) |
67 | 66 | r19.21bi 3141 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐷 ∈ ℝ) |
68 | 8 | r19.21bi 3141 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
69 | 45, 68 | sylan2 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
70 | 69 | fmpttd 6634 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) |
71 | | dvfre 24113 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
72 | 70, 49, 71 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
73 | | dvle.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
74 | 73 | dmeqd 5558 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
75 | 55 | brrelex1i 5393 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ≤ 𝐷 → 𝐵 ∈ V) |
76 | 54, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ V) |
77 | 76 | ralrimiva 3175 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ V) |
78 | | dmmptg 5873 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ V → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
80 | 74, 79 | eqtrd 2861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) |
81 | 73, 80 | feq12d 6266 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) |
82 | 72, 81 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
83 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) |
84 | 83 | fmpt 6629 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
85 | 82, 84 | sylibr 226 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ) |
86 | 85 | r19.21bi 3141 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ ℝ) |
87 | 67, 86 | resubcld 10782 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝐷 − 𝐵) ∈ ℝ) |
88 | 67, 86 | subge0d 10942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (0 ≤ (𝐷 − 𝐵) ↔ 𝐵 ≤ 𝐷)) |
89 | 54, 88 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 0 ≤ (𝐷 − 𝐵)) |
90 | | elrege0 12568 |
. . . . . . . . 9
⊢ ((𝐷 − 𝐵) ∈ (0[,)+∞) ↔ ((𝐷 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐷 − 𝐵))) |
91 | 87, 89, 90 | sylanbrc 578 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝐷 − 𝐵) ∈ (0[,)+∞)) |
92 | 91 | fmpttd 6634 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵)):(𝑀(,)𝑁)⟶(0[,)+∞)) |
93 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
94 | | iccssre 12543 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
95 | 37, 38, 94 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
96 | 46, 68 | resubcld 10782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐶 − 𝐴) ∈ ℝ) |
97 | 96 | recnd 10385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐶 − 𝐴) ∈ ℂ) |
98 | 39 | tgioo2 22976 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
99 | | iccntr 22994 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
100 | 37, 38, 99 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
101 | 93, 95, 97, 98, 39, 100 | dvmptntr 24133 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))) = (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐶 − 𝐴)))) |
102 | | reelprrecn 10344 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
103 | 102 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
104 | 46 | recnd 10385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
105 | 45, 104 | sylan2 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
106 | 68 | recnd 10385 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
107 | 45, 106 | sylan2 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
108 | 103, 105,
57, 52, 107, 76, 73 | dvmptsub 24129 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐶 − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵))) |
109 | 101, 108 | eqtrd 2861 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵))) |
110 | 109 | feq1d 6263 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))):(𝑀(,)𝑁)⟶(0[,)+∞) ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵)):(𝑀(,)𝑁)⟶(0[,)+∞))) |
111 | 92, 110 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))):(𝑀(,)𝑁)⟶(0[,)+∞)) |
112 | | dvle.l |
. . . . . 6
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
113 | 37, 38, 43, 111, 22, 9, 112 | dvge0 24168 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) ≤ ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌)) |
114 | 20, 25 | oveq12d 6923 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐶 − 𝐴) = (𝑄 − 𝑃)) |
115 | | eqid 2825 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) = (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) |
116 | | ovex 6937 |
. . . . . . 7
⊢ (𝐶 − 𝐴) ∈ V |
117 | 114, 115,
116 | fvmpt3i 6534 |
. . . . . 6
⊢ (𝑋 ∈ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) = (𝑄 − 𝑃)) |
118 | 22, 117 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) = (𝑄 − 𝑃)) |
119 | 11, 1 | oveq12d 6923 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐶 − 𝐴) = (𝑆 − 𝑅)) |
120 | 119, 115,
116 | fvmpt3i 6534 |
. . . . . 6
⊢ (𝑌 ∈ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌) = (𝑆 − 𝑅)) |
121 | 9, 120 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌) = (𝑆 − 𝑅)) |
122 | 113, 118,
121 | 3brtr3d 4904 |
. . . 4
⊢ (𝜑 → (𝑄 − 𝑃) ≤ (𝑆 − 𝑅)) |
123 | 23, 27, 36, 122 | subled 10955 |
. . 3
⊢ (𝜑 → (𝑄 − (𝑆 − 𝑅)) ≤ 𝑃) |
124 | 35, 123 | eqbrtrd 4895 |
. 2
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) ≤ 𝑃) |
125 | 10, 24, 27, 124 | subled 10955 |
1
⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄)) |