Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nrmmetd Structured version   Visualization version   GIF version

Theorem nrmmetd 22580
 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.)
Hypotheses
Ref Expression
nrmmetd.x 𝑋 = (Base‘𝐺)
nrmmetd.m = (-g𝐺)
nrmmetd.z 0 = (0g𝐺)
nrmmetd.g (𝜑𝐺 ∈ Grp)
nrmmetd.f (𝜑𝐹:𝑋⟶ℝ)
nrmmetd.1 ((𝜑𝑥𝑋) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
nrmmetd.2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
Assertion
Ref Expression
nrmmetd (𝜑 → (𝐹 ) ∈ (Met‘𝑋))
Distinct variable groups:   𝑥,𝑦,   𝑥, 0 ,𝑦   𝑥,𝐹,𝑦   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐺(𝑥,𝑦)

Proof of Theorem nrmmetd
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nrmmetd.f . . 3 (𝜑𝐹:𝑋⟶ℝ)
2 nrmmetd.g . . . 4 (𝜑𝐺 ∈ Grp)
3 nrmmetd.x . . . . 5 𝑋 = (Base‘𝐺)
4 nrmmetd.m . . . . 5 = (-g𝐺)
53, 4grpsubf 17695 . . . 4 (𝐺 ∈ Grp → :(𝑋 × 𝑋)⟶𝑋)
62, 5syl 17 . . 3 (𝜑 :(𝑋 × 𝑋)⟶𝑋)
7 fco 6219 . . 3 ((𝐹:𝑋⟶ℝ ∧ :(𝑋 × 𝑋)⟶𝑋) → (𝐹 ):(𝑋 × 𝑋)⟶ℝ)
81, 6, 7syl2anc 696 . 2 (𝜑 → (𝐹 ):(𝑋 × 𝑋)⟶ℝ)
9 opelxpi 5305 . . . . . . . 8 ((𝑎𝑋𝑏𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
10 fvco3 6437 . . . . . . . 8 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑎, 𝑏⟩) = (𝐹‘( ‘⟨𝑎, 𝑏⟩)))
116, 9, 10syl2an 495 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹 )‘⟨𝑎, 𝑏⟩) = (𝐹‘( ‘⟨𝑎, 𝑏⟩)))
12 df-ov 6816 . . . . . . 7 (𝑎(𝐹 )𝑏) = ((𝐹 )‘⟨𝑎, 𝑏⟩)
13 df-ov 6816 . . . . . . . 8 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
1413fveq2i 6355 . . . . . . 7 (𝐹‘(𝑎 𝑏)) = (𝐹‘( ‘⟨𝑎, 𝑏⟩))
1511, 12, 143eqtr4g 2819 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(𝐹 )𝑏) = (𝐹‘(𝑎 𝑏)))
1615eqeq1d 2762 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹 )𝑏) = 0 ↔ (𝐹‘(𝑎 𝑏)) = 0))
173, 4grpsubcl 17696 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑏𝑋) → (𝑎 𝑏) ∈ 𝑋)
18173expb 1114 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎 𝑏) ∈ 𝑋)
192, 18sylan 489 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎 𝑏) ∈ 𝑋)
20 nrmmetd.1 . . . . . . . 8 ((𝜑𝑥𝑋) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
2120ralrimiva 3104 . . . . . . 7 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
22 fveq2 6352 . . . . . . . . . 10 (𝑥 = (𝑎 𝑏) → (𝐹𝑥) = (𝐹‘(𝑎 𝑏)))
2322eqeq1d 2762 . . . . . . . . 9 (𝑥 = (𝑎 𝑏) → ((𝐹𝑥) = 0 ↔ (𝐹‘(𝑎 𝑏)) = 0))
24 eqeq1 2764 . . . . . . . . 9 (𝑥 = (𝑎 𝑏) → (𝑥 = 0 ↔ (𝑎 𝑏) = 0 ))
2523, 24bibi12d 334 . . . . . . . 8 (𝑥 = (𝑎 𝑏) → (((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 )))
2625rspccva 3448 . . . . . . 7 ((∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑎 𝑏) ∈ 𝑋) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
2721, 26sylan 489 . . . . . 6 ((𝜑 ∧ (𝑎 𝑏) ∈ 𝑋) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
2819, 27syldan 488 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
29 nrmmetd.z . . . . . . . 8 0 = (0g𝐺)
303, 29, 4grpsubeq0 17702 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑏𝑋) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
31303expb 1114 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
322, 31sylan 489 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
3316, 28, 323bitrd 294 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏))
341adantr 472 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝐹:𝑋⟶ℝ)
3519adantrr 755 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎 𝑏) ∈ 𝑋)
3634, 35ffvelrnd 6523 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ∈ ℝ)
372adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝐺 ∈ Grp)
38 simprll 821 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑎𝑋)
39 simprr 813 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑐𝑋)
403, 4grpsubcl 17696 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑐𝑋) → (𝑎 𝑐) ∈ 𝑋)
4137, 38, 39, 40syl3anc 1477 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎 𝑐) ∈ 𝑋)
4234, 41ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ∈ ℝ)
43 simprlr 822 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑏𝑋)
443, 4grpsubcl 17696 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 𝑐) ∈ 𝑋)
4537, 43, 39, 44syl3anc 1477 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑏 𝑐) ∈ 𝑋)
4634, 45ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ∈ ℝ)
4742, 46readdcld 10261 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))) ∈ ℝ)
483, 4grpsubcl 17696 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑎𝑋) → (𝑐 𝑎) ∈ 𝑋)
4937, 39, 38, 48syl3anc 1477 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑋)
5034, 49ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑐 𝑎)) ∈ ℝ)
513, 4grpsubcl 17696 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑏𝑋) → (𝑐 𝑏) ∈ 𝑋)
5237, 39, 43, 51syl3anc 1477 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐 𝑏) ∈ 𝑋)
5334, 52ffvelrnd 6523 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑐 𝑏)) ∈ ℝ)
5450, 53readdcld 10261 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))) ∈ ℝ)
553, 4grpnnncan2 17713 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝑎 𝑐) (𝑏 𝑐)) = (𝑎 𝑏))
5637, 38, 43, 39, 55syl13anc 1479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝑎 𝑐) (𝑏 𝑐)) = (𝑎 𝑏))
5756fveq2d 6356 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) = (𝐹‘(𝑎 𝑏)))
58 nrmmetd.2 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
5958ralrimivva 3109 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
6059adantr 472 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
61 oveq1 6820 . . . . . . . . . . . . 13 (𝑥 = (𝑎 𝑐) → (𝑥 𝑦) = ((𝑎 𝑐) 𝑦))
6261fveq2d 6356 . . . . . . . . . . . 12 (𝑥 = (𝑎 𝑐) → (𝐹‘(𝑥 𝑦)) = (𝐹‘((𝑎 𝑐) 𝑦)))
63 fveq2 6352 . . . . . . . . . . . . 13 (𝑥 = (𝑎 𝑐) → (𝐹𝑥) = (𝐹‘(𝑎 𝑐)))
6463oveq1d 6828 . . . . . . . . . . . 12 (𝑥 = (𝑎 𝑐) → ((𝐹𝑥) + (𝐹𝑦)) = ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)))
6562, 64breq12d 4817 . . . . . . . . . . 11 (𝑥 = (𝑎 𝑐) → ((𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)) ↔ (𝐹‘((𝑎 𝑐) 𝑦)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦))))
66 oveq2 6821 . . . . . . . . . . . . 13 (𝑦 = (𝑏 𝑐) → ((𝑎 𝑐) 𝑦) = ((𝑎 𝑐) (𝑏 𝑐)))
6766fveq2d 6356 . . . . . . . . . . . 12 (𝑦 = (𝑏 𝑐) → (𝐹‘((𝑎 𝑐) 𝑦)) = (𝐹‘((𝑎 𝑐) (𝑏 𝑐))))
68 fveq2 6352 . . . . . . . . . . . . 13 (𝑦 = (𝑏 𝑐) → (𝐹𝑦) = (𝐹‘(𝑏 𝑐)))
6968oveq2d 6829 . . . . . . . . . . . 12 (𝑦 = (𝑏 𝑐) → ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)) = ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7067, 69breq12d 4817 . . . . . . . . . . 11 (𝑦 = (𝑏 𝑐) → ((𝐹‘((𝑎 𝑐) 𝑦)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)) ↔ (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐)))))
7165, 70rspc2va 3462 . . . . . . . . . 10 ((((𝑎 𝑐) ∈ 𝑋 ∧ (𝑏 𝑐) ∈ 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦))) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7241, 45, 60, 71syl21anc 1476 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7357, 72eqbrtrrd 4828 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
74 eleq1w 2822 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
7574anbi2d 742 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → ((𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑐𝑋)))
7675anbi2d 742 . . . . . . . . . . . 12 (𝑏 = 𝑐 → ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) ↔ (𝜑 ∧ (𝑎𝑋𝑐𝑋))))
77 oveq2 6821 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑎 𝑏) = (𝑎 𝑐))
7877fveq2d 6356 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝐹‘(𝑎 𝑏)) = (𝐹‘(𝑎 𝑐)))
79 oveq1 6820 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑏 𝑎) = (𝑐 𝑎))
8079fveq2d 6356 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝐹‘(𝑏 𝑎)) = (𝐹‘(𝑐 𝑎)))
8178, 80breq12d 4817 . . . . . . . . . . . 12 (𝑏 = 𝑐 → ((𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎)) ↔ (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎))))
8276, 81imbi12d 333 . . . . . . . . . . 11 (𝑏 = 𝑐 → (((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎))) ↔ ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))))
832adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝐺 ∈ Grp)
843, 29grpidcl 17651 . . . . . . . . . . . . . 14 (𝐺 ∈ Grp → 0𝑋)
8583, 84syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 0𝑋)
86 simprr 813 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
87 simprl 811 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
883, 4grpsubcl 17696 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑎𝑋) → (𝑏 𝑎) ∈ 𝑋)
8983, 86, 87, 88syl3anc 1477 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑏 𝑎) ∈ 𝑋)
9059adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
91 oveq1 6820 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑥 𝑦) = ( 0 𝑦))
9291fveq2d 6356 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (𝐹‘(𝑥 𝑦)) = (𝐹‘( 0 𝑦)))
93 fveq2 6352 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝐹𝑥) = (𝐹0 ))
9493oveq1d 6828 . . . . . . . . . . . . . . 15 (𝑥 = 0 → ((𝐹𝑥) + (𝐹𝑦)) = ((𝐹0 ) + (𝐹𝑦)))
9592, 94breq12d 4817 . . . . . . . . . . . . . 14 (𝑥 = 0 → ((𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)) ↔ (𝐹‘( 0 𝑦)) ≤ ((𝐹0 ) + (𝐹𝑦))))
96 oveq2 6821 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏 𝑎) → ( 0 𝑦) = ( 0 (𝑏 𝑎)))
9796fveq2d 6356 . . . . . . . . . . . . . . 15 (𝑦 = (𝑏 𝑎) → (𝐹‘( 0 𝑦)) = (𝐹‘( 0 (𝑏 𝑎))))
98 fveq2 6352 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏 𝑎) → (𝐹𝑦) = (𝐹‘(𝑏 𝑎)))
9998oveq2d 6829 . . . . . . . . . . . . . . 15 (𝑦 = (𝑏 𝑎) → ((𝐹0 ) + (𝐹𝑦)) = ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
10097, 99breq12d 4817 . . . . . . . . . . . . . 14 (𝑦 = (𝑏 𝑎) → ((𝐹‘( 0 𝑦)) ≤ ((𝐹0 ) + (𝐹𝑦)) ↔ (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎)))))
10195, 100rspc2va 3462 . . . . . . . . . . . . 13 ((( 0𝑋 ∧ (𝑏 𝑎) ∈ 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦))) → (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
10285, 89, 90, 101syl21anc 1476 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
103 eqid 2760 . . . . . . . . . . . . . . . 16 (invg𝐺) = (invg𝐺)
1043, 4, 103, 29grpinvval2 17699 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (𝑏 𝑎) ∈ 𝑋) → ((invg𝐺)‘(𝑏 𝑎)) = ( 0 (𝑏 𝑎)))
10583, 89, 104syl2anc 696 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((invg𝐺)‘(𝑏 𝑎)) = ( 0 (𝑏 𝑎)))
1063, 4, 103grpinvsub 17698 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑎𝑋) → ((invg𝐺)‘(𝑏 𝑎)) = (𝑎 𝑏))
10783, 86, 87, 106syl3anc 1477 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((invg𝐺)‘(𝑏 𝑎)) = (𝑎 𝑏))
108105, 107eqtr3d 2796 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ( 0 (𝑏 𝑎)) = (𝑎 𝑏))
109108fveq2d 6356 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘( 0 (𝑏 𝑎))) = (𝐹‘(𝑎 𝑏)))
1102, 84syl 17 . . . . . . . . . . . . . . . 16 (𝜑0𝑋)
111 pm5.501 355 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ (𝑥 = 0 ↔ (𝐹𝑥) = 0)))
112 bicom 212 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 0 ↔ (𝐹𝑥) = 0) ↔ ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
113111, 112syl6bb 276 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ ((𝐹𝑥) = 0 ↔ 𝑥 = 0 )))
11493eqeq1d 2762 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ (𝐹0 ) = 0))
115113, 114bitr3d 270 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (𝐹0 ) = 0))
116115rspccva 3448 . . . . . . . . . . . . . . . 16 ((∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ∧ 0𝑋) → (𝐹0 ) = 0)
11721, 110, 116syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹0 ) = 0)
118117adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹0 ) = 0)
119118oveq1d 6828 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹0 ) + (𝐹‘(𝑏 𝑎))) = (0 + (𝐹‘(𝑏 𝑎))))
1201adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝐹:𝑋⟶ℝ)
121120, 89ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑏 𝑎)) ∈ ℝ)
122121recnd 10260 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑏 𝑎)) ∈ ℂ)
123122addid2d 10429 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (0 + (𝐹‘(𝑏 𝑎))) = (𝐹‘(𝑏 𝑎)))
124119, 123eqtrd 2794 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹0 ) + (𝐹‘(𝑏 𝑎))) = (𝐹‘(𝑏 𝑎)))
125102, 109, 1243brtr3d 4835 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎)))
12682, 125chvarv 2408 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))
127126adantrlr 761 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))
128 eleq1w 2822 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑎𝑋𝑏𝑋))
129128anbi1d 743 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → ((𝑎𝑋𝑐𝑋) ↔ (𝑏𝑋𝑐𝑋)))
130129anbi2d 742 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) ↔ (𝜑 ∧ (𝑏𝑋𝑐𝑋))))
131 oveq1 6820 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑎 𝑐) = (𝑏 𝑐))
132131fveq2d 6356 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → (𝐹‘(𝑎 𝑐)) = (𝐹‘(𝑏 𝑐)))
133 oveq2 6821 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑐 𝑎) = (𝑐 𝑏))
134133fveq2d 6356 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → (𝐹‘(𝑐 𝑎)) = (𝐹‘(𝑐 𝑏)))
135132, 134breq12d 4817 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ((𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)) ↔ (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏))))
136130, 135imbi12d 333 . . . . . . . . . . 11 (𝑎 = 𝑏 → (((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎))) ↔ ((𝜑 ∧ (𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))))
137136, 126chvarv 2408 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))
138137adantrll 760 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))
13942, 46, 50, 53, 127, 138le2addd 10838 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))) ≤ ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
14036, 47, 54, 73, 139letrd 10386 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
14115adantrr 755 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎(𝐹 )𝑏) = (𝐹‘(𝑎 𝑏)))
1426adantr 472 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → :(𝑋 × 𝑋)⟶𝑋)
143 opelxpi 5305 . . . . . . . . . . 11 ((𝑐𝑋𝑎𝑋) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
14439, 38, 143syl2anc 696 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
145 fvco3 6437 . . . . . . . . . 10 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑐, 𝑎⟩) = (𝐹‘( ‘⟨𝑐, 𝑎⟩)))
146142, 144, 145syl2anc 696 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹 )‘⟨𝑐, 𝑎⟩) = (𝐹‘( ‘⟨𝑐, 𝑎⟩)))
147 df-ov 6816 . . . . . . . . 9 (𝑐(𝐹 )𝑎) = ((𝐹 )‘⟨𝑐, 𝑎⟩)
148 df-ov 6816 . . . . . . . . . 10 (𝑐 𝑎) = ( ‘⟨𝑐, 𝑎⟩)
149148fveq2i 6355 . . . . . . . . 9 (𝐹‘(𝑐 𝑎)) = (𝐹‘( ‘⟨𝑐, 𝑎⟩))
150146, 147, 1493eqtr4g 2819 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐(𝐹 )𝑎) = (𝐹‘(𝑐 𝑎)))
151 opelxpi 5305 . . . . . . . . . . 11 ((𝑐𝑋𝑏𝑋) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
15239, 43, 151syl2anc 696 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
153 fvco3 6437 . . . . . . . . . 10 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑐, 𝑏⟩) = (𝐹‘( ‘⟨𝑐, 𝑏⟩)))
154142, 152, 153syl2anc 696 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹 )‘⟨𝑐, 𝑏⟩) = (𝐹‘( ‘⟨𝑐, 𝑏⟩)))
155 df-ov 6816 . . . . . . . . 9 (𝑐(𝐹 )𝑏) = ((𝐹 )‘⟨𝑐, 𝑏⟩)
156 df-ov 6816 . . . . . . . . . 10 (𝑐 𝑏) = ( ‘⟨𝑐, 𝑏⟩)
157156fveq2i 6355 . . . . . . . . 9 (𝐹‘(𝑐 𝑏)) = (𝐹‘( ‘⟨𝑐, 𝑏⟩))
158154, 155, 1573eqtr4g 2819 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐(𝐹 )𝑏) = (𝐹‘(𝑐 𝑏)))
159150, 158oveq12d 6831 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)) = ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
160140, 141, 1593brtr4d 4836 . . . . . 6 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))
161160expr 644 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑐𝑋 → (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
162161ralrimiv 3103 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))
16333, 162jca 555 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
164163ralrimivva 3109 . 2 (𝜑 → ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
165 fvex 6362 . . . 4 (Base‘𝐺) ∈ V
1663, 165eqeltri 2835 . . 3 𝑋 ∈ V
167 ismet 22329 . . 3 (𝑋 ∈ V → ((𝐹 ) ∈ (Met‘𝑋) ↔ ((𝐹 ):(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))))
168166, 167ax-mp 5 . 2 ((𝐹 ) ∈ (Met‘𝑋) ↔ ((𝐹 ):(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))))
1698, 164, 168sylanbrc 701 1 (𝜑 → (𝐹 ) ∈ (Met‘𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050  Vcvv 3340  ⟨cop 4327   class class class wbr 4804   × cxp 5264   ∘ ccom 5270  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813  ℝcr 10127  0cc0 10128   + caddc 10131   ≤ cle 10267  Basecbs 16059  0gc0g 16302  Grpcgrp 17623  invgcminusg 17624  -gcsg 17625  Metcme 19934 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-0g 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-grp 17626  df-minusg 17627  df-sbg 17628  df-met 19942 This theorem is referenced by:  abvmet  22581  tngngpd  22658
 Copyright terms: Public domain W3C validator