Step | Hyp | Ref
| Expression |
1 | | df-ov 6552 |
. . . . 5
⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) |
2 | | xpsle.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | xpsle.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
4 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
5 | 4 | xpsfval 16050 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
6 | 2, 3, 5 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
7 | 1, 6 | syl5eqr 2658 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
8 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
9 | 2, 3, 8 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
10 | 4 | xpsff1o2 16054 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
11 | | f1of 6050 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
13 | 12 | ffvelrni 6266 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
14 | 9, 13 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
15 | 7, 14 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
16 | | df-ov 6552 |
. . . . 5
⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) |
17 | | xpsle.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
18 | | xpsle.6 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
19 | 4 | xpsfval 16050 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
20 | 17, 18, 19 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
21 | 16, 20 | syl5eqr 2658 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
22 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
23 | 17, 18, 22 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
24 | 12 | ffvelrni 6266 |
. . . . 5
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
26 | 21, 25 | eqeltrrd 2689 |
. . 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 2610 |
. . . . 5
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
33 | | eqid 2610 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
34 | 27, 28, 29, 30, 31, 4, 32, 33 | xpsval 16055 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
35 | 27, 28, 29, 30, 31, 4, 32, 33 | xpslem 16056 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
36 | | f1ocnv 6062 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
37 | 10, 36 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
38 | | f1ofo 6057 |
. . . . 5
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
40 | | ovex 6577 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V |
41 | 40 | a1i 11 |
. . . 4
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
42 | | xpsle.p |
. . . 4
⊢ ≤ =
(le‘𝑇) |
43 | | eqid 2610 |
. . . 4
⊢
(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
44 | 37 | f1olecpbl 16010 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ (𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑑 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → (((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑎) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑑)) → (𝑎(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑏 ↔ 𝑐(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑑))) |
45 | 34, 35, 39, 41, 42, 43, 44 | imasleval 16024 |
. . 3
⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ ◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
46 | 15, 26, 45 | mpd3an23 1418 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ ◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
47 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
48 | 10, 9, 47 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
49 | 7, 48 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
50 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
51 | 10, 23, 50 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
52 | 21, 51 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
53 | 49, 52 | breq12d 4596 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ≤ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) ↔ 〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉)) |
54 | | eqid 2610 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
55 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑅)
∈ V |
56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
57 | | 2on 7455 |
. . . . 5
⊢
2𝑜 ∈ On |
58 | 57 | a1i 11 |
. . . 4
⊢ (𝜑 → 2𝑜
∈ On) |
59 | | xpscfn 16042 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
60 | 30, 31, 59 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
61 | 15, 35 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
62 | 26, 35 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
63 | 33, 54, 56, 58, 60, 61, 62, 43 | prdsleval 15960 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}) ↔ ∀𝑘 ∈ 2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
64 | | df2o3 7460 |
. . . . . 6
⊢
2𝑜 = {∅,
1𝑜} |
65 | 64 | raleqi 3119 |
. . . . 5
⊢
(∀𝑘 ∈
2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ∀𝑘 ∈ {∅, 1𝑜}
(◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) |
66 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
67 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
68 | 67 | elexi 3186 |
. . . . . 6
⊢
1𝑜 ∈ V |
69 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅)) |
70 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
71 | 70 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = ∅ →
(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (le‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
72 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅)) |
73 | 69, 71, 72 | breq123d 4597 |
. . . . . 6
⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))) |
74 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1𝑜)) |
75 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
76 | 75 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
77 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1𝑜 →
(◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1𝑜)) |
78 | 74, 76, 77 | breq123d 4597 |
. . . . . 6
⊢ (𝑘 = 1𝑜 →
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
79 | 66, 68, 73, 78 | ralpr 4185 |
. . . . 5
⊢
(∀𝑘 ∈
{∅, 1𝑜} (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
80 | 65, 79 | bitri 263 |
. . . 4
⊢
(∀𝑘 ∈
2𝑜 (◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
81 | | xpsc0 16043 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
82 | 2, 81 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
83 | | xpsc0 16043 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
84 | 30, 83 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
85 | 84 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (le‘𝑅)) |
86 | | xpsle.m |
. . . . . . 7
⊢ 𝑀 = (le‘𝑅) |
87 | 85, 86 | syl6eqr 2662 |
. . . . . 6
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = 𝑀) |
88 | | xpsc0 16043 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
89 | 17, 88 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
90 | 82, 87, 89 | breq123d 4597 |
. . . . 5
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ↔ 𝐴𝑀𝐶)) |
91 | | xpsc1 16044 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
92 | 3, 91 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
93 | | xpsc1 16044 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
94 | 31, 93 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
95 | 94 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) =
(le‘𝑆)) |
96 | | xpsle.n |
. . . . . . 7
⊢ 𝑁 = (le‘𝑆) |
97 | 95, 96 | syl6eqr 2662 |
. . . . . 6
⊢ (𝜑 → (le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) = 𝑁) |
98 | | xpsc1 16044 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
99 | 18, 98 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
100 | 92, 97, 99 | breq123d 4597 |
. . . . 5
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜) ↔ 𝐵𝑁𝐷)) |
101 | 90, 100 | anbi12d 743 |
. . . 4
⊢ (𝜑 → (((◡({𝐴} +𝑐 {𝐵})‘∅)(le‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅) ∧ (◡({𝐴} +𝑐 {𝐵})‘1𝑜)(le‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
102 | 80, 101 | syl5bb 271 |
. . 3
⊢ (𝜑 → (∀𝑘 ∈ 2𝑜
(◡({𝐴} +𝑐 {𝐵})‘𝑘)(le‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
103 | 63, 102 | bitrd 267 |
. 2
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(le‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}) ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |
104 | 46, 53, 103 | 3bitr3d 297 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉 ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) |