| 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 19037 |
. . . 4
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
| 6 | 2, 5 | syl 17 |
. . 3
⊢ (𝜑 → − :(𝑋 × 𝑋)⟶𝑋) |
| 7 | | fco 6760 |
. . 3
⊢ ((𝐹:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝐹 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
| 8 | 1, 6, 7 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐹 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
| 9 | | opelxpi 5722 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) |
| 10 | | fvco3 7008 |
. . . . . . . 8
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) = (𝐹‘( − ‘〈𝑎, 𝑏〉))) |
| 11 | 6, 9, 10 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) = (𝐹‘( − ‘〈𝑎, 𝑏〉))) |
| 12 | | df-ov 7434 |
. . . . . . 7
⊢ (𝑎(𝐹 ∘ − )𝑏) = ((𝐹 ∘ − )‘〈𝑎, 𝑏〉) |
| 13 | | df-ov 7434 |
. . . . . . . 8
⊢ (𝑎 − 𝑏) = ( − ‘〈𝑎, 𝑏〉) |
| 14 | 13 | fveq2i 6909 |
. . . . . . 7
⊢ (𝐹‘(𝑎 − 𝑏)) = (𝐹‘( − ‘〈𝑎, 𝑏〉)) |
| 15 | 11, 12, 14 | 3eqtr4g 2802 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) = (𝐹‘(𝑎 − 𝑏))) |
| 16 | 15 | eqeq1d 2739 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ (𝐹‘(𝑎 − 𝑏)) = 0)) |
| 17 | | nrmmetd.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
| 18 | 17 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
| 19 | 3, 4 | grpsubcl 19038 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 − 𝑏) ∈ 𝑋) |
| 20 | 19 | 3expb 1121 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
| 21 | 2, 20 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
| 22 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = (𝑎 − 𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎 − 𝑏))) |
| 23 | 22 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = (𝑎 − 𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎 − 𝑏)) = 0)) |
| 24 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = (𝑎 − 𝑏) → (𝑥 = 0 ↔ (𝑎 − 𝑏) = 0 )) |
| 25 | 23, 24 | bibi12d 345 |
. . . . . . 7
⊢ (𝑥 = (𝑎 − 𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝐹‘(𝑎 − 𝑏)) = 0 ↔ (𝑎 − 𝑏) = 0 ))) |
| 26 | 25 | rspccva 3621 |
. . . . . 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 19044 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
| 30 | 29 | 3expb 1121 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
| 31 | 2, 30 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎 − 𝑏) = 0 ↔ 𝑎 = 𝑏)) |
| 32 | 16, 27, 31 | 3bitrd 305 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏)) |
| 33 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝐹:𝑋⟶ℝ) |
| 34 | 21 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎 − 𝑏) ∈ 𝑋) |
| 35 | 33, 34 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ∈ ℝ) |
| 36 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝐺 ∈ Grp) |
| 37 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
| 38 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
| 39 | 3, 4 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑎 − 𝑐) ∈ 𝑋) |
| 40 | 36, 37, 38, 39 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎 − 𝑐) ∈ 𝑋) |
| 41 | 33, 40 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ∈ ℝ) |
| 42 | | simprlr 780 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
| 43 | 3, 4 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) → (𝑏 − 𝑐) ∈ 𝑋) |
| 44 | 36, 42, 38, 43 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑏 − 𝑐) ∈ 𝑋) |
| 45 | 33, 44 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ∈ ℝ) |
| 46 | 41, 45 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))) ∈ ℝ) |
| 47 | 3, 4 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → (𝑐 − 𝑎) ∈ 𝑋) |
| 48 | 36, 38, 37, 47 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐 − 𝑎) ∈ 𝑋) |
| 49 | 33, 48 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐 − 𝑎)) ∈ ℝ) |
| 50 | 3, 4 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑐 − 𝑏) ∈ 𝑋) |
| 51 | 36, 38, 42, 50 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐 − 𝑏) ∈ 𝑋) |
| 52 | 33, 51 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐 − 𝑏)) ∈ ℝ) |
| 53 | 49, 52 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏))) ∈ ℝ) |
| 54 | 3, 4 | grpnnncan2 19055 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎 − 𝑐) − (𝑏 − 𝑐)) = (𝑎 − 𝑏)) |
| 55 | 36, 37, 42, 38, 54 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝑎 − 𝑐) − (𝑏 − 𝑐)) = (𝑎 − 𝑏)) |
| 56 | 55 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) = (𝐹‘(𝑎 − 𝑏))) |
| 57 | | nrmmetd.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 58 | 57 | ralrimivva 3202 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 59 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 60 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 − 𝑐) → (𝐹‘(𝑥 − 𝑦)) = (𝐹‘((𝑎 − 𝑐) − 𝑦))) |
| 61 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑎 − 𝑐) → (𝐹‘𝑥) = (𝐹‘(𝑎 − 𝑐))) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎 − 𝑐) → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦))) |
| 63 | 60, 62 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎 − 𝑐) → ((𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘((𝑎 − 𝑐) − 𝑦)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)))) |
| 64 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝑎 − 𝑐) − 𝑦) = ((𝑎 − 𝑐) − (𝑏 − 𝑐))) |
| 65 | 64 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑏 − 𝑐) → (𝐹‘((𝑎 − 𝑐) − 𝑦)) = (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐)))) |
| 66 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑏 − 𝑐) → (𝐹‘𝑦) = (𝐹‘(𝑏 − 𝑐))) |
| 67 | 66 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)) = ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
| 68 | 65, 67 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑏 − 𝑐) → ((𝐹‘((𝑎 − 𝑐) − 𝑦)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘𝑦)) ↔ (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))))) |
| 69 | 63, 68 | rspc2va 3634 |
. . . . . . . . . 10
⊢ ((((𝑎 − 𝑐) ∈ 𝑋 ∧ (𝑏 − 𝑐) ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
| 70 | 40, 44, 59, 69 | syl21anc 838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑎 − 𝑐) − (𝑏 − 𝑐))) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
| 71 | 56, 70 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐)))) |
| 72 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝑏 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋)) |
| 73 | 72 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))) |
| 74 | 73 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ↔ (𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)))) |
| 75 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑐 → (𝑎 − 𝑏) = (𝑎 − 𝑐)) |
| 76 | 75 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → (𝐹‘(𝑎 − 𝑏)) = (𝐹‘(𝑎 − 𝑐))) |
| 77 | | fvoveq1 7454 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑐 → (𝐹‘(𝑏 − 𝑎)) = (𝐹‘(𝑐 − 𝑎))) |
| 78 | 76, 77 | breq12d 5156 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑐 → ((𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎)) ↔ (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎)))) |
| 79 | 74, 78 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑐 → (((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎))) ↔ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))))) |
| 80 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐺 ∈ Grp) |
| 81 | 3, 28 | grpidcl 18983 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
| 82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 0 ∈ 𝑋) |
| 83 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
| 84 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
| 85 | 3, 4 | grpsubcl 19038 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → (𝑏 − 𝑎) ∈ 𝑋) |
| 86 | 80, 83, 84, 85 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑏 − 𝑎) ∈ 𝑋) |
| 87 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
| 88 | | fvoveq1 7454 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝐹‘(𝑥 − 𝑦)) = (𝐹‘( 0 − 𝑦))) |
| 89 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘ 0 )) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘ 0 ) + (𝐹‘𝑦))) |
| 91 | 88, 90 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → ((𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘( 0 − 𝑦)) ≤ ((𝐹‘ 0 ) + (𝐹‘𝑦)))) |
| 92 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏 − 𝑎) → ( 0 − 𝑦) = ( 0 − (𝑏 − 𝑎))) |
| 93 | 92 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑏 − 𝑎) → (𝐹‘( 0 − 𝑦)) = (𝐹‘( 0 − (𝑏 − 𝑎)))) |
| 94 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏 − 𝑎) → (𝐹‘𝑦) = (𝐹‘(𝑏 − 𝑎))) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑏 − 𝑎) → ((𝐹‘ 0 ) + (𝐹‘𝑦)) = ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
| 96 | 93, 95 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑏 − 𝑎) → ((𝐹‘( 0 − 𝑦)) ≤ ((𝐹‘ 0 ) + (𝐹‘𝑦)) ↔ (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))))) |
| 97 | 91, 96 | rspc2va 3634 |
. . . . . . . . . . . . 13
⊢ ((( 0 ∈ 𝑋 ∧ (𝑏 − 𝑎) ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) → (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
| 98 | 82, 86, 87, 97 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘( 0 − (𝑏 − 𝑎))) ≤ ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎)))) |
| 99 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 100 | 3, 4, 99, 28 | grpinvval2 19041 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (𝑏 − 𝑎) ∈ 𝑋) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = ( 0 − (𝑏 − 𝑎))) |
| 101 | 2, 86, 100 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = ( 0 − (𝑏 − 𝑎))) |
| 102 | 3, 4, 99 | grpinvsub 19040 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
| 103 | 80, 83, 84, 102 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((invg‘𝐺)‘(𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
| 104 | 101, 103 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ( 0 − (𝑏 − 𝑎)) = (𝑎 − 𝑏)) |
| 105 | 104 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘( 0 − (𝑏 − 𝑎))) = (𝐹‘(𝑎 − 𝑏))) |
| 106 | 2, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈ 𝑋) |
| 107 | | pm5.501 366 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ (𝑥 = 0 ↔ (𝐹‘𝑥) = 0))) |
| 108 | | bicom 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 0 ↔ (𝐹‘𝑥) = 0) ↔ ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) |
| 109 | 107, 108 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ))) |
| 110 | 89 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = 0 ↔ (𝐹‘ 0 ) = 0)) |
| 111 | 109, 110 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (𝐹‘ 0 ) = 0)) |
| 112 | 111 | rspccva 3621 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝑋 ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ 0 ∈ 𝑋) → (𝐹‘ 0 ) = 0) |
| 113 | 18, 106, 112 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘ 0 ) = 0) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘ 0 ) = 0) |
| 115 | 114 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))) = (0 + (𝐹‘(𝑏 − 𝑎)))) |
| 116 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝐹:𝑋⟶ℝ) |
| 117 | 116, 86 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑎)) ∈ ℝ) |
| 118 | 117 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑎)) ∈ ℂ) |
| 119 | 118 | addlidd 11462 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (0 + (𝐹‘(𝑏 − 𝑎))) = (𝐹‘(𝑏 − 𝑎))) |
| 120 | 115, 119 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘ 0 ) + (𝐹‘(𝑏 − 𝑎))) = (𝐹‘(𝑏 − 𝑎))) |
| 121 | 98, 105, 120 | 3brtr3d 5174 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ (𝐹‘(𝑏 − 𝑎))) |
| 122 | 79, 121 | chvarvv 1998 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) |
| 123 | 122 | adantrlr 723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) |
| 124 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋)) |
| 125 | 124 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋) ↔ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))) |
| 126 | 125 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) ↔ (𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)))) |
| 127 | | fvoveq1 7454 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝐹‘(𝑎 − 𝑐)) = (𝐹‘(𝑏 − 𝑐))) |
| 128 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑐 − 𝑎) = (𝑐 − 𝑏)) |
| 129 | 128 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝐹‘(𝑐 − 𝑎)) = (𝐹‘(𝑐 − 𝑏))) |
| 130 | 127, 129 | breq12d 5156 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎)) ↔ (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏)))) |
| 131 | 126, 130 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑎))) ↔ ((𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))))) |
| 132 | 131, 122 | chvarvv 1998 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))) |
| 133 | 132 | adantrll 722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑏 − 𝑐)) ≤ (𝐹‘(𝑐 − 𝑏))) |
| 134 | 41, 45, 49, 52, 123, 133 | le2addd 11882 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑎 − 𝑐)) + (𝐹‘(𝑏 − 𝑐))) ≤ ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
| 135 | 35, 46, 53, 71, 134 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎 − 𝑏)) ≤ ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
| 136 | 15 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) = (𝐹‘(𝑎 − 𝑏))) |
| 137 | | opelxpi 5722 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
| 138 | 38, 37, 137 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
| 139 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) = (𝐹‘( − ‘〈𝑐, 𝑎〉))) |
| 140 | 6, 138, 139 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) = (𝐹‘( − ‘〈𝑐, 𝑎〉))) |
| 141 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑐(𝐹 ∘ − )𝑎) = ((𝐹 ∘ − )‘〈𝑐, 𝑎〉) |
| 142 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑐 − 𝑎) = ( − ‘〈𝑐, 𝑎〉) |
| 143 | 142 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝐹‘(𝑐 − 𝑎)) = (𝐹‘( − ‘〈𝑐, 𝑎〉)) |
| 144 | 140, 141,
143 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ − )𝑎) = (𝐹‘(𝑐 − 𝑎))) |
| 145 | | opelxpi 5722 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
| 146 | 38, 42, 145 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
| 147 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) = (𝐹‘( − ‘〈𝑐, 𝑏〉))) |
| 148 | 6, 146, 147 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) = (𝐹‘( − ‘〈𝑐, 𝑏〉))) |
| 149 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑐(𝐹 ∘ − )𝑏) = ((𝐹 ∘ − )‘〈𝑐, 𝑏〉) |
| 150 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑐 − 𝑏) = ( − ‘〈𝑐, 𝑏〉) |
| 151 | 150 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝐹‘(𝑐 − 𝑏)) = (𝐹‘( − ‘〈𝑐, 𝑏〉)) |
| 152 | 148, 149,
151 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ − )𝑏) = (𝐹‘(𝑐 − 𝑏))) |
| 153 | 144, 152 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)) = ((𝐹‘(𝑐 − 𝑎)) + (𝐹‘(𝑐 − 𝑏)))) |
| 154 | 135, 136,
153 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))) |
| 155 | 154 | expr 456 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑐 ∈ 𝑋 → (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
| 156 | 155 | ralrimiv 3145 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))) |
| 157 | 32, 156 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
| 158 | 157 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))) |
| 159 | 3 | fvexi 6920 |
. . 3
⊢ 𝑋 ∈ V |
| 160 | | ismet 24333 |
. . 3
⊢ (𝑋 ∈ V → ((𝐹 ∘ − ) ∈
(Met‘𝑋) ↔
((𝐹 ∘ −
):(𝑋 × 𝑋)⟶ℝ ∧
∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏)))))) |
| 161 | 159, 160 | ax-mp 5 |
. 2
⊢ ((𝐹 ∘ − ) ∈
(Met‘𝑋) ↔
((𝐹 ∘ −
):(𝑋 × 𝑋)⟶ℝ ∧
∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (((𝑎(𝐹 ∘ − )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐 ∈ 𝑋 (𝑎(𝐹 ∘ − )𝑏) ≤ ((𝑐(𝐹 ∘ − )𝑎) + (𝑐(𝐹 ∘ − )𝑏))))) |
| 162 | 8, 158, 161 | sylanbrc 583 |
1
⊢ (𝜑 → (𝐹 ∘ − ) ∈
(Met‘𝑋)) |