Metamath Proof Explorer

Theorem nrmmetd

Description: Show that a group norm generates a metric. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nrmmetd.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
nrmmetd.m ⊢ − = ( -g ‘ 𝐺 )
nrmmetd.z ⊢ 0 = ( 0g ‘ 𝐺 )
nrmmetd.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
nrmmetd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
nrmmetd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
nrmmetd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
Assertion nrmmetd ( 𝜑 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 nrmmetd.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 nrmmetd.m ⊢ − = ( -g ‘ 𝐺 )
3 nrmmetd.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 nrmmetd.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
5 nrmmetd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
6 nrmmetd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
7 nrmmetd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
8 1 2 grpsubf ⊢ ( 𝐺 ∈ Grp → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9 4 8 syl ⊢ ( 𝜑 → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
10 fco ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝐹 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
11 5 9 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
12 opelxpi ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) )
13 fvco3 ⊢ ( ( − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
14 9 12 13 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
15 df-ov ⊢ ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑎 , 𝑏 ⟩ )
16 df-ov ⊢ ( 𝑎 − 𝑏 ) = ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ )
17 16 fveq2i ⊢ ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
18 14 15 17 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) )
19 18 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = 0 ) )
20 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
21 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 − 𝑏 ) ∈ 𝑋 )
22 21 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 − 𝑏 ) ∈ 𝑋 )
23 4 22 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 − 𝑏 ) ∈ 𝑋 )
24 fveq2 ⊢ ( 𝑥 = ( 𝑎 − 𝑏 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) )
25 24 eqeq1d ⊢ ( 𝑥 = ( 𝑎 − 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = 0 ) )
26 eqeq1 ⊢ ( 𝑥 = ( 𝑎 − 𝑏 ) → ( 𝑥 = 0 ↔ ( 𝑎 − 𝑏 ) = 0 ) )
27 25 26 bibi12d ⊢ ( 𝑥 = ( 𝑎 − 𝑏 ) → ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = 0 ↔ ( 𝑎 − 𝑏 ) = 0 ) ) )
28 27 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ( 𝑎 − 𝑏 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = 0 ↔ ( 𝑎 − 𝑏 ) = 0 ) )
29 20 23 28 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = 0 ↔ ( 𝑎 − 𝑏 ) = 0 ) )
30 1 3 2 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝑎 − 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
31 30 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 − 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
32 4 31 sylan ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 − 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
33 19 29 32 3bitrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) )
34 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ ℝ )
35 23 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑎 − 𝑏 ) ∈ 𝑋 )
36 34 35 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ∈ ℝ )
37 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
38 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
39 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 )
40 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) → ( 𝑎 − 𝑐 ) ∈ 𝑋 )
41 37 38 39 40 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑎 − 𝑐 ) ∈ 𝑋 )
42 34 41 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ∈ ℝ )
43 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
44 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) → ( 𝑏 − 𝑐 ) ∈ 𝑋 )
45 37 43 39 44 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑏 − 𝑐 ) ∈ 𝑋 )
46 34 45 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ∈ ℝ )
47 42 46 readdcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) ∈ ℝ )
48 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( 𝑐 − 𝑎 ) ∈ 𝑋 )
49 37 39 38 48 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 − 𝑎 ) ∈ 𝑋 )
50 34 49 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) ∈ ℝ )
51 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑐 − 𝑏 ) ∈ 𝑋 )
52 37 39 43 51 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 − 𝑏 ) ∈ 𝑋 )
53 34 52 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ∈ ℝ )
54 50 53 readdcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) + ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) ∈ ℝ )
55 1 2 grpnnncan2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) = ( 𝑎 − 𝑏 ) )
56 37 38 43 39 55 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) = ( 𝑎 − 𝑏 ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) ) = ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) )
58 7 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
60 fvoveq1 ⊢ ( 𝑥 = ( 𝑎 − 𝑐 ) → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) = ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − 𝑦 ) ) )
61 fveq2 ⊢ ( 𝑥 = ( 𝑎 − 𝑐 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) )
62 61 oveq1d ⊢ ( 𝑥 = ( 𝑎 − 𝑐 ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ 𝑦 ) ) )
63 60 62 breq12d ⊢ ( 𝑥 = ( 𝑎 − 𝑐 ) → ( ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − 𝑦 ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ 𝑦 ) ) ) )
64 oveq2 ⊢ ( 𝑦 = ( 𝑏 − 𝑐 ) → ( ( 𝑎 − 𝑐 ) − 𝑦 ) = ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) )
65 64 fveq2d ⊢ ( 𝑦 = ( 𝑏 − 𝑐 ) → ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − 𝑦 ) ) = ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) ) )
66 fveq2 ⊢ ( 𝑦 = ( 𝑏 − 𝑐 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) )
67 66 oveq2d ⊢ ( 𝑦 = ( 𝑏 − 𝑐 ) → ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) )
68 65 67 breq12d ⊢ ( 𝑦 = ( 𝑏 − 𝑐 ) → ( ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − 𝑦 ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) ) )
69 63 68 rspc2va ⊢ ( ( ( ( 𝑎 − 𝑐 ) ∈ 𝑋 ∧ ( 𝑏 − 𝑐 ) ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) )
70 41 45 59 69 syl21anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑎 − 𝑐 ) − ( 𝑏 − 𝑐 ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) )
71 57 70 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ≤ ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) )
72 eleq1w ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋 ) )
73 72 anbi2d ⊢ ( 𝑏 = 𝑐 → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ↔ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) )
74 73 anbi2d ⊢ ( 𝑏 = 𝑐 → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ) )
75 oveq2 ⊢ ( 𝑏 = 𝑐 → ( 𝑎 − 𝑏 ) = ( 𝑎 − 𝑐 ) )
76 75 fveq2d ⊢ ( 𝑏 = 𝑐 → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) )
77 fvoveq1 ⊢ ( 𝑏 = 𝑐 → ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) = ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) )
78 76 77 breq12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ≤ ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) ) )
79 74 78 imbi12d ⊢ ( 𝑏 = 𝑐 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ≤ ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) ) ) )
80 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
81 1 3 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 )
82 80 81 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 0 ∈ 𝑋 )
83 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
84 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
85 1 2 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( 𝑏 − 𝑎 ) ∈ 𝑋 )
86 80 83 84 85 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑏 − 𝑎 ) ∈ 𝑋 )
87 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
88 fvoveq1 ⊢ ( 𝑥 = 0 → ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) = ( 𝐹 ‘ ( 0 − 𝑦 ) ) )
89 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) )
90 89 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) )
91 88 90 breq12d ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 0 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) ) )
92 oveq2 ⊢ ( 𝑦 = ( 𝑏 − 𝑎 ) → ( 0 − 𝑦 ) = ( 0 − ( 𝑏 − 𝑎 ) ) )
93 92 fveq2d ⊢ ( 𝑦 = ( 𝑏 − 𝑎 ) → ( 𝐹 ‘ ( 0 − 𝑦 ) ) = ( 𝐹 ‘ ( 0 − ( 𝑏 − 𝑎 ) ) ) )
94 fveq2 ⊢ ( 𝑦 = ( 𝑏 − 𝑎 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) )
95 94 oveq2d ⊢ ( 𝑦 = ( 𝑏 − 𝑎 ) → ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) )
96 93 95 breq12d ⊢ ( 𝑦 = ( 𝑏 − 𝑎 ) → ( ( 𝐹 ‘ ( 0 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 0 − ( 𝑏 − 𝑎 ) ) ) ≤ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) ) )
97 91 96 rspc2va ⊢ ( ( ( 0 ∈ 𝑋 ∧ ( 𝑏 − 𝑎 ) ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 0 − ( 𝑏 − 𝑎 ) ) ) ≤ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) )
98 82 86 87 97 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 0 − ( 𝑏 − 𝑎 ) ) ) ≤ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) )
99 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
100 1 2 99 3 grpinvval2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑏 − 𝑎 ) ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑏 − 𝑎 ) ) = ( 0 − ( 𝑏 − 𝑎 ) ) )
101 4 86 100 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑏 − 𝑎 ) ) = ( 0 − ( 𝑏 − 𝑎 ) ) )
102 1 2 99 grpinvsub ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑏 − 𝑎 ) ) = ( 𝑎 − 𝑏 ) )
103 80 83 84 102 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑏 − 𝑎 ) ) = ( 𝑎 − 𝑏 ) )
104 101 103 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 0 − ( 𝑏 − 𝑎 ) ) = ( 𝑎 − 𝑏 ) )
105 104 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 0 − ( 𝑏 − 𝑎 ) ) ) = ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) )
106 4 81 syl ⊢ ( 𝜑 → 0 ∈ 𝑋 )
107 pm5.501 ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝑥 = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) ) )
108 bicom ⊢ ( ( 𝑥 = 0 ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
109 107 108 bitrdi ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ) )
110 89 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 0 ) = 0 ) )
111 109 110 bitr3d ⊢ ( 𝑥 = 0 → ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( 𝐹 ‘ 0 ) = 0 ) )
112 111 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ 0 ∈ 𝑋 ) → ( 𝐹 ‘ 0 ) = 0 )
113 20 106 112 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
114 113 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ 0 ) = 0 )
115 114 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) = ( 0 + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) )
116 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ ℝ )
117 116 86 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ∈ ℝ )
118 117 recnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ∈ ℂ )
119 118 addid2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 0 + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) )
120 115 119 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) ) = ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) )
121 98 105 120 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ≤ ( 𝐹 ‘ ( 𝑏 − 𝑎 ) ) )
122 79 121 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) )
123 122 adantrlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) )
124 eleq1w ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∈ 𝑋 ↔ 𝑏 ∈ 𝑋 ) )
125 124 anbi1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ↔ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) )
126 125 anbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) ) )
127 fvoveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) = ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) )
128 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑐 − 𝑎 ) = ( 𝑐 − 𝑏 ) )
129 128 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) = ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) )
130 127 129 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) ↔ ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) )
131 126 130 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) ) )
132 131 122 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) )
133 132 adantrll ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) )
134 42 46 50 53 123 133 le2addd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑎 − 𝑐 ) ) + ( 𝐹 ‘ ( 𝑏 − 𝑐 ) ) ) ≤ ( ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) + ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) )
135 36 47 54 71 134 letrd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) ≤ ( ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) + ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) )
136 18 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = ( 𝐹 ‘ ( 𝑎 − 𝑏 ) ) )
137 opelxpi ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ⟨ 𝑐 , 𝑎 ⟩ ∈ ( 𝑋 × 𝑋 ) )
138 39 38 137 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ⟨ 𝑐 , 𝑎 ⟩ ∈ ( 𝑋 × 𝑋 ) )
139 fvco3 ⊢ ( ( − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑐 , 𝑎 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑎 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑎 ⟩ ) ) )
140 9 138 139 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑎 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑎 ⟩ ) ) )
141 df-ov ⊢ ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) = ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑎 ⟩ )
142 df-ov ⊢ ( 𝑐 − 𝑎 ) = ( − ‘ ⟨ 𝑐 , 𝑎 ⟩ )
143 142 fveq2i ⊢ ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑎 ⟩ ) )
144 140 141 143 3eqtr4g ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) = ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) )
145 opelxpi ⊢ ( ( 𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ⟨ 𝑐 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) )
146 39 43 145 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ⟨ 𝑐 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) )
147 fvco3 ⊢ ( ( − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑐 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑏 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑏 ⟩ ) ) )
148 9 146 147 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑏 ⟩ ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑏 ⟩ ) ) )
149 df-ov ⊢ ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) = ( ( 𝐹 ∘ − ) ‘ ⟨ 𝑐 , 𝑏 ⟩ )
150 df-ov ⊢ ( 𝑐 − 𝑏 ) = ( − ‘ ⟨ 𝑐 , 𝑏 ⟩ )
151 150 fveq2i ⊢ ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) = ( 𝐹 ‘ ( − ‘ ⟨ 𝑐 , 𝑏 ⟩ ) )
152 148 149 151 3eqtr4g ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) = ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) )
153 144 152 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) = ( ( 𝐹 ‘ ( 𝑐 − 𝑎 ) ) + ( 𝐹 ‘ ( 𝑐 − 𝑏 ) ) ) )
154 135 136 153 3brtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) )
155 154 expr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑐 ∈ 𝑋 → ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) ) )
156 155 ralrimiv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ∀ 𝑐 ∈ 𝑋 ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) )
157 33 156 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑋 ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) ) )
158 157 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑋 ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) ) )
159 1 fvexi ⊢ 𝑋 ∈ V
160 ismet ⊢ ( 𝑋 ∈ V → ( ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) ↔ ( ( 𝐹 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑋 ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) ) ) ) )
161 159 160 ax-mp ⊢ ( ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) ↔ ( ( 𝐹 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) = 0 ↔ 𝑎 = 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑋 ( 𝑎 ( 𝐹 ∘ − ) 𝑏 ) ≤ ( ( 𝑐 ( 𝐹 ∘ − ) 𝑎 ) + ( 𝑐 ( 𝐹 ∘ − ) 𝑏 ) ) ) ) )
162 11 158 161 sylanbrc ⊢ ( 𝜑 → ( 𝐹 ∘ − ) ∈ ( Met ‘ 𝑋 ) )