Step | Hyp | Ref
| Expression |
1 | | nrmmetd.f |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
2 | | nrmmetd.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
3 | | nrmmetd.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
4 | | nrmmetd.m |
. . . . 5
⊢ − =
(-g‘𝐺) |
5 | 3, 4 | grpsubf 18289 |
. . . 4
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
6 | 2, 5 | syl 17 |
. . 3
⊢ (𝜑 → − :(𝑋 × 𝑋)⟶𝑋) |
7 | | fco 6522 |
. . 3
⊢ ((𝐹:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝐹 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
8 | 1, 6, 7 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝐹 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
9 | | opelxpi 5556 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) |
10 | | fvco3 6761 |
. . . . . . . 8
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) = (𝐹‘( − ‘〈𝑎, 𝑏〉))) |
11 | 6, 9, 10 | syl2an 599 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) = (𝐹‘( − ‘〈𝑎, 𝑏〉))) |
12 | | df-ov 7167 |
. . . . . . 7
⊢ (𝑎(𝐹 ∘ − )𝑏) = ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) |
13 | | df-ov 7167 |
. . . . . . . 8
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) |
14 | 13 | fveq2i 6671 |
. . . . . . 7
⊢ (𝐹‘(𝑎 − 𝑏)) = (𝐹‘( − ‘〈𝑎, 𝑏〉)) |
15 | 11, 12, 14 | 3eqtr4g 2798 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) = (𝐹‘(𝑎 − 𝑏))) |
16 | 15 | eqeq1d 2740 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ (𝐹‘(𝑎 − 𝑏)) = 0)) |
17 | | nrmmetd.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
18 | 17 | ralrimiva 3096 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
19 | 3, 4 | grpsubcl 18290 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) ∈ 𝑋) |
20 | 19 | 3expb 1121 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
21 | 2, 20 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
22 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑥 = (𝑎 − 𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎 − 𝑏))) |
23 | 22 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑥 = (𝑎 − 𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎 − 𝑏)) = 0)) |
24 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑥 = (𝑎 − 𝑏) → (𝑥 = 0 ↔ (𝑎 − 𝑏) = 0 )) |
25 | 23, 24 | bibi12d 349 |
. . . . . . 7
⊢ (𝑥 = (𝑎 − 𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝐹‘(𝑎 − 𝑏)) = 0 ↔ (𝑎 − 𝑏) = 0 ))) |
26 | 25 | rspccva 3523 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑋 ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑎 − 𝑏) ∈ 𝑋) → ((𝐹‘(𝑎 − 𝑏)) = 0 ↔ (𝑎 − 𝑏) = 0 )) |
27 | 18, 21, 26 | syl2an2r 685 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎 − 𝑏)) = 0 ↔ (𝑎 − 𝑏) = 0 )) |
28 | | nrmmetd.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
29 | 3, 28, 4 | grpsubeq0 18296 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
30 | 29 | 3expb 1121 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
31 | 2, 30 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
32 | 16, 27, 31 | 3bitrd 308 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏)) |
33 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝐹:𝑋⟶ℝ) |
34 | 21 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
35 | 33, 34 | ffvelrnd 6856 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ∈ ℝ) |
36 | 2 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝐺 ∈ Grp) |
37 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
38 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
39 | 3, 4 | grpsubcl 18290 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑎 − 𝑐) ∈ 𝑋) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎 − 𝑐) ∈ 𝑋) |
41 | 33, 40 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ∈ ℝ) |
42 | | simprlr 780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
43 | 3, 4 | grpsubcl 18290 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑏 − 𝑐) ∈ 𝑋) |
44 | 36, 42, 38, 43 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑏 − 𝑐) ∈ 𝑋) |
45 | 33, 44 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ∈ ℝ) |
46 | 41, 45 | readdcld 10741 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))) ∈ ℝ) |
47 | 3, 4 | grpsubcl 18290 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → (𝑐 − 𝑎) ∈ 𝑋) |
48 | 36, 38, 37, 47 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐 − 𝑎) ∈ 𝑋) |
49 | 33, 48 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐 − 𝑎)) ∈ ℝ) |
50 | 3, 4 | grpsubcl 18290 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑐 − 𝑏) ∈ 𝑋) |
51 | 36, 38, 42, 50 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐 − 𝑏) ∈ 𝑋) |
52 | 33, 51 | ffvelrnd 6856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐 − 𝑏)) ∈ ℝ) |
53 | 49, 52 | readdcld 10741 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏))) ∈ ℝ) |
54 | 3, 4 | grpnnncan2 18307 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎 − 𝑐) − (𝑏 − 𝑐)) = (𝑎 − 𝑏)) |
55 | 36, 37, 42, 38, 54 | syl13anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝑎 − 𝑐) − (𝑏 − 𝑐)) = (𝑎 − 𝑏)) |
56 | 55 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) = (𝐹‘(𝑎 − 𝑏))) |
57 | | nrmmetd.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
58 | 57 | ralrimivva 3103 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
59 | 58 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
60 | | fvoveq1 7187 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 − 𝑐) → (𝐹‘(𝑥 − 𝑦)) = (𝐹‘((𝑎 − 𝑐) − 𝑦))) |
61 | | fveq2 6668 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑎 − 𝑐) → (𝐹‘𝑥) = (𝐹‘(𝑎 − 𝑐))) |
62 | 61 | oveq1d 7179 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 − 𝑐) → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦))) |
63 | 60, 62 | breq12d 5040 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 − 𝑐) → ((𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘((𝑎 − 𝑐) − 𝑦)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)))) |
64 | | oveq2 7172 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝑎 − 𝑐) − 𝑦) = ((𝑎 − 𝑐) − (𝑏 − 𝑐))) |
65 | 64 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑏 − 𝑐) → (𝐹‘((𝑎 − 𝑐) − 𝑦)) = (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐)))) |
66 | | fveq2 6668 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑏 − 𝑐) → (𝐹‘𝑦) = (𝐹‘(𝑏 − 𝑐))) |
67 | 66 | oveq2d 7180 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)) = ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
68 | 65, 67 | breq12d 5040 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝐹‘((𝑎 − 𝑐) − 𝑦)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)) ↔ (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))))) |
69 | 63, 68 | rspc2va 3535 |
. . . . . . . . . 10
⊢ ((((𝑎 − 𝑐) ∈ 𝑋 ∧ (𝑏 − 𝑐) ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
70 | 40, 44, 59, 69 | syl21anc 837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
71 | 56, 70 | eqbrtrrd 5051 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
72 | | eleq1w 2815 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝑏 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋)) |
73 | 72 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))) |
74 | 73 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ↔ (𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)))) |
75 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝑎 − 𝑏) = (𝑎 − 𝑐)) |
76 | 75 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → (𝐹‘(𝑎 − 𝑏)) = (𝐹‘(𝑎 − 𝑐))) |
77 | | fvoveq1 7187 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → (𝐹‘(𝑏 − 𝑎)) = (𝐹‘(𝑐 − 𝑎))) |
78 | 76, 77 | breq12d 5040 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → ((𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎)) ↔ (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎)))) |
79 | 74, 78 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑐 → (((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎))) ↔ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))))) |
80 | 2 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐺 ∈ Grp) |
81 | 3, 28 | grpidcl 18242 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 0 ∈ 𝑋) |
83 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
84 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
85 | 3, 4 | grpsubcl 18290 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → (𝑏 − 𝑎) ∈ 𝑋) |
86 | 80, 83, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑏 − 𝑎) ∈ 𝑋) |
87 | 58 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
88 | | fvoveq1 7187 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝐹‘(𝑥 − 𝑦)) = (𝐹‘( 0 − 𝑦))) |
89 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘ 0 )) |
90 | 89 | oveq1d 7179 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘ 0 ) + (𝐹‘𝑦))) |
91 | 88, 90 | breq12d 5040 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → ((𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘( 0 − 𝑦)) ≤ ((𝐹‘ 0 ) + (𝐹‘𝑦)))) |
92 | | oveq2 7172 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏 − 𝑎) → ( 0 − 𝑦) = ( 0 − (𝑏 − 𝑎))) |
93 | 92 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑏 − 𝑎) → (𝐹‘( 0 − 𝑦)) = (𝐹‘( 0 − (𝑏 − 𝑎)))) |
94 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏 − 𝑎) → (𝐹‘𝑦) = (𝐹‘(𝑏 − 𝑎))) |
95 | 94 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑏 − 𝑎) → ((𝐹‘ 0 ) + (𝐹‘𝑦)) = ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
96 | 93, 95 | breq12d 5040 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑏 − 𝑎) → ((𝐹‘( 0 − 𝑦)) ≤ ((𝐹‘ 0 ) + (𝐹‘𝑦)) ↔ (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))))) |
97 | 91, 96 | rspc2va 3535 |
. . . . . . . . . . . . 13
⊢ ((( 0 ∈ 𝑋 ∧ (𝑏 − 𝑎) ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
98 | 82, 86, 87, 97 | syl21anc 837 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
99 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(invg‘𝐺) = (invg‘𝐺) |
100 | 3, 4, 99, 28 | grpinvval2 18293 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (𝑏 − 𝑎) ∈ 𝑋) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = ( 0 − (𝑏 − 𝑎))) |
101 | 2, 86, 100 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = ( 0 − (𝑏 − 𝑎))) |
102 | 3, 4, 99 | grpinvsub 18292 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
103 | 80, 83, 84, 102 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
104 | 101, 103 | eqtr3d 2775 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ( 0 − (𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
105 | 104 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘( 0 − (𝑏 − 𝑎))) = (𝐹‘(𝑎 − 𝑏))) |
106 | 2, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈ 𝑋) |
107 | | pm5.501 370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ (𝑥 = 0 ↔ (𝐹‘𝑥) = 0))) |
108 | | bicom 225 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 0 ↔ (𝐹‘𝑥) = 0) ↔ ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
109 | 107, 108 | bitrdi 290 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ))) |
110 | 89 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ (𝐹‘ 0 ) = 0)) |
111 | 109, 110 | bitr3d 284 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (𝐹‘ 0 ) = 0)) |
112 | 111 | rspccva 3523 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝑋 ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ 0 ∈ 𝑋) → (𝐹‘ 0 ) = 0) |
113 | 18, 106, 112 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘ 0 ) = 0) |
114 | 113 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘ 0 ) = 0) |
115 | 114 | oveq1d 7179 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))) = (0 + (𝐹‘(𝑏 − 𝑎)))) |
116 | 1 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐹:𝑋⟶ℝ) |
117 | 116, 86 | ffvelrnd 6856 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑎)) ∈ ℝ) |
118 | 117 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑎)) ∈ ℂ) |
119 | 118 | addid2d 10912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (0 + (𝐹‘(𝑏 − 𝑎))) = (𝐹‘(𝑏 − 𝑎))) |
120 | 115, 119 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))) = (𝐹‘(𝑏 − 𝑎))) |
121 | 98, 105, 120 | 3brtr3d 5058 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎))) |
122 | 79, 121 | chvarvv 2009 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) |
123 | 122 | adantrlr 723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) |
124 | | eleq1w 2815 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋)) |
125 | 124 | anbi1d 633 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) ↔ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))) |
126 | 125 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ↔ (𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)))) |
127 | | fvoveq1 7187 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝐹‘(𝑎 − 𝑐)) = (𝐹‘(𝑏 − 𝑐))) |
128 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑐 − 𝑎) = (𝑐 − 𝑏)) |
129 | 128 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝐹‘(𝑐 − 𝑎)) = (𝐹‘(𝑐 − 𝑏))) |
130 | 127, 129 | breq12d 5040 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎)) ↔ (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏)))) |
131 | 126, 130 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) ↔ ((𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))))) |
132 | 131, 122 | chvarvv 2009 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))) |
133 | 132 | adantrll 722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))) |
134 | 41, 45, 49, 52, 123, 133 | le2addd 11330 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))) ≤ ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
135 | 35, 46, 53, 71, 134 | letrd 10868 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
136 | 15 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) = (𝐹‘(𝑎 − 𝑏))) |
137 | | opelxpi 5556 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
138 | 38, 37, 137 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
139 | | fvco3 6761 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) = (𝐹‘( − ‘〈𝑐, 𝑎〉))) |
140 | 6, 138, 139 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) = (𝐹‘( − ‘〈𝑐, 𝑎〉))) |
141 | | df-ov 7167 |
. . . . . . . . 9
⊢ (𝑐(𝐹 ∘ − )𝑎) = ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) |
142 | | df-ov 7167 |
. . . . . . . . . 10
⊢ (𝑐 − 𝑎) = ( − ‘〈𝑐, 𝑎〉) |
143 | 142 | fveq2i 6671 |
. . . . . . . . 9
⊢ (𝐹‘(𝑐 − 𝑎)) = (𝐹‘( − ‘〈𝑐, 𝑎〉)) |
144 | 140, 141,
143 | 3eqtr4g 2798 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ − )𝑎) = (𝐹‘(𝑐 − 𝑎))) |
145 | | opelxpi 5556 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
146 | 38, 42, 145 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
147 | | fvco3 6761 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) = (𝐹‘( − ‘〈𝑐, 𝑏〉))) |
148 | 6, 146, 147 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) = (𝐹‘( − ‘〈𝑐, 𝑏〉))) |
149 | | df-ov 7167 |
. . . . . . . . 9
⊢ (𝑐(𝐹 ∘ − )𝑏) = ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) |
150 | | df-ov 7167 |
. . . . . . . . . 10
⊢ (𝑐 − 𝑏) = ( − ‘〈𝑐, 𝑏〉) |
151 | 150 | fveq2i 6671 |
. . . . . . . . 9
⊢ (𝐹‘(𝑐 − 𝑏)) = (𝐹‘( − ‘〈𝑐, 𝑏〉)) |
152 | 148, 149,
151 | 3eqtr4g 2798 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ − )𝑏) = (𝐹‘(𝑐 − 𝑏))) |
153 | 144, 152 | oveq12d 7182 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)) = ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
154 | 135, 136,
153 | 3brtr4d 5059 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))) |
155 | 154 | expr 460 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑐 ∈ 𝑋 → (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
156 | 155 | ralrimiv 3095 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))) |
157 | 32, 156 | jca 515 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
158 | 157 | ralrimivva 3103 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
159 | 3 | fvexi 6682 |
. . 3
⊢ 𝑋 ∈ V |
160 | | ismet 23069 |
. . 3
⊢ (𝑋 ∈ V → ((𝐹 ∘ − ) ∈
(Met‘𝑋) ↔
((𝐹 ∘ −
):(𝑋 × 𝑋)⟶ℝ ∧
∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))))) |
161 | 159, 160 | ax-mp 5 |
. 2
⊢ ((𝐹 ∘ − ) ∈
(Met‘𝑋) ↔
((𝐹 ∘ −
):(𝑋 × 𝑋)⟶ℝ ∧
∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))))) |
162 | 8, 158, 161 | sylanbrc 586 |
1
⊢ (𝜑 → (𝐹 ∘ − ) ∈
(Met‘𝑋)) |