Step | Hyp | Ref
| Expression |
1 | | df-ov 6808 |
. . . . 5
⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) |
2 | | xpsle.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | xpsle.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
4 | | eqid 2752 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
5 | 4 | xpsfval 16421 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
6 | 2, 3, 5 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
7 | 1, 6 | syl5eqr 2800 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
8 | | opelxpi 5297 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
9 | 2, 3, 8 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
10 | 4 | xpsff1o2 16425 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
11 | | f1of 6290 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
13 | 12 | ffvelrni 6513 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
14 | 9, 13 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
15 | 7, 14 | eqeltrrd 2832 |
. . 3
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
16 | | df-ov 6808 |
. . . . 5
⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) |
17 | | xpsle.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
18 | | xpsle.6 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
19 | 4 | xpsfval 16421 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
20 | 17, 18, 19 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
21 | 16, 20 | syl5eqr 2800 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
22 | | opelxpi 5297 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
23 | 17, 18, 22 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
24 | 12 | ffvelrni 6513 |
. . . . 5
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
26 | 21, 25 | eqeltrrd 2832 |
. . 3
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
27 | | xpsle.t |
. . . . 5
⊢ 𝑇 = (𝑅 ×s 𝑆) |
28 | | xpsle.x |
. . . . 5
⊢ 𝑋 = (Base‘𝑅) |
29 | | xpsle.y |
. . . . 5
⊢ 𝑌 = (Base‘𝑆) |
30 | | xpsle.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
31 | | xpsle.2 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
32 | | eqid 2752 |
. . . . 5
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
33 | | eqid 2752 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
34 | 27, 28, 29, 30, 31, 4, 32, 33 | xpsval 16426 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
35 | 27, 28, 29, 30, 31, 4, 32, 33 | xpslem 16427 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
36 | | f1ocnv 6302 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
37 | 10, 36 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
38 | | f1ofo 6297 |
. . . . 5
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
40 | | ovexd 6835 |
. . . 4
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
41 | | xpsle.p |
. . . 4
⊢ ≤ =
(le‘𝑇) |
42 | | eqid 2752 |
. . . 4
⊢
(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
43 | 37 | f1olecpbl 16381 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ (𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑑 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → (((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑎) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑑)) → (𝑎(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑏 ↔ 𝑐(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑑))) |
44 | 34, 35, 39, 40, 41, 42, 43 | imasleval 16395 |
. . 3
⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ ◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
45 | 15, 26, 44 | mpd3an23 1567 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ ◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
46 | | f1ocnvfv 6689 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
47 | 10, 9, 46 | sylancr 698 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
48 | 7, 47 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
49 | | f1ocnvfv 6689 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
50 | 10, 23, 49 | sylancr 698 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
51 | 21, 50 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
52 | 48, 51 | breq12d 4809 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ 〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉)) |
53 | | eqid 2752 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
54 | | fvexd 6356 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
55 | | 2on 7729 |
. . . . 5
⊢
2𝑜 ∈ On |
56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → 2𝑜
∈ On) |
57 | | xpscfn 16413 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
58 | 30, 31, 57 | syl2anc 696 |
. . . 4
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
59 | 15, 35 | eleqtrd 2833 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
60 | 26, 35 | eleqtrd 2833 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
61 | 33, 53, 54, 56, 58, 59, 60, 42 | prdsleval 16331 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}) ↔ ∀𝑘 ∈ 2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
62 | | df2o3 7734 |
. . . . . 6
⊢
2𝑜 = {∅,
1𝑜} |
63 | 62 | raleqi 3273 |
. . . . 5
⊢
(∀𝑘 ∈
2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ∀𝑘 ∈ {∅, 1𝑜}
(◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) |
64 | | 0ex 4934 |
. . . . . 6
⊢ ∅
∈ V |
65 | | 1on 7728 |
. . . . . . 7
⊢
1𝑜 ∈ On |
66 | 65 | elexi 3345 |
. . . . . 6
⊢
1𝑜 ∈ V |
67 | | fveq2 6344 |
. . . . . . 7
⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅)) |
68 | | fveq2 6344 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
69 | 68 | fveq2d 6348 |
. . . . . . 7
⊢ (𝑘 = ∅ →
(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (le‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
70 | | fveq2 6344 |
. . . . . . 7
⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅)) |
71 | 67, 69, 70 | breq123d 4810 |
. . . . . 6
⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))) |
72 | | fveq2 6344 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1𝑜)) |
73 | | fveq2 6344 |
. . . . . . . 8
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
74 | 73 | fveq2d 6348 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
75 | | fveq2 6344 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1𝑜)) |
76 | 72, 74, 75 | breq123d 4810 |
. . . . . 6
⊢ (𝑘 = 1𝑜 →
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
77 | 64, 66, 71, 76 | ralpr 4374 |
. . . . 5
⊢
(∀𝑘 ∈
{∅, 1𝑜} (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
78 | 63, 77 | bitri 264 |
. . . 4
⊢
(∀𝑘 ∈
2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
79 | | xpsc0 16414 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
80 | 2, 79 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
81 | | xpsc0 16414 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
82 | 30, 81 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
83 | 82 | fveq2d 6348 |
. . . . . . 7
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (le‘𝑅)) |
84 | | xpsle.m |
. . . . . . 7
⊢ 𝑀 = (le‘𝑅) |
85 | 83, 84 | syl6eqr 2804 |
. . . . . 6
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = 𝑀) |
86 | | xpsc0 16414 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
87 | 17, 86 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
88 | 80, 85, 87 | breq123d 4810 |
. . . . 5
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ↔ 𝐴𝑀𝐶)) |
89 | | xpsc1 16415 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
90 | 3, 89 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
91 | | xpsc1 16415 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
92 | 31, 91 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
93 | 92 | fveq2d 6348 |
. . . . . . 7
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) =
(le‘𝑆)) |
94 | | xpsle.n |
. . . . . . 7
⊢ 𝑁 = (le‘𝑆) |
95 | 93, 94 | syl6eqr 2804 |
. . . . . 6
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) = 𝑁) |
96 | | xpsc1 16415 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
97 | 18, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
98 | 90, 95, 97 | breq123d 4810 |
. . . . 5
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜) ↔ 𝐵𝑁𝐷)) |
99 | 88, 98 | anbi12d 749 |
. . . 4
⊢ (𝜑 → (((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
100 | 78, 99 | syl5bb 272 |
. . 3
⊢ (𝜑 → (∀𝑘 ∈ 2𝑜
(◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
101 | 61, 100 | bitrd 268 |
. 2
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
102 | 45, 52, 101 | 3bitr3d 298 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉 ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |