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

Theorem nrmmetd 22289
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 17415 . . . 4 (𝐺 ∈ Grp → :(𝑋 × 𝑋)⟶𝑋)
62, 5syl 17 . . 3 (𝜑 :(𝑋 × 𝑋)⟶𝑋)
7 fco 6015 . . 3 ((𝐹:𝑋⟶ℝ ∧ :(𝑋 × 𝑋)⟶𝑋) → (𝐹 ):(𝑋 × 𝑋)⟶ℝ)
81, 6, 7syl2anc 692 . 2 (𝜑 → (𝐹 ):(𝑋 × 𝑋)⟶ℝ)
9 opelxpi 5108 . . . . . . . 8 ((𝑎𝑋𝑏𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
10 fvco3 6232 . . . . . . . 8 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑎, 𝑏⟩) = (𝐹‘( ‘⟨𝑎, 𝑏⟩)))
116, 9, 10syl2an 494 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹 )‘⟨𝑎, 𝑏⟩) = (𝐹‘( ‘⟨𝑎, 𝑏⟩)))
12 df-ov 6607 . . . . . . 7 (𝑎(𝐹 )𝑏) = ((𝐹 )‘⟨𝑎, 𝑏⟩)
13 df-ov 6607 . . . . . . . 8 (𝑎 𝑏) = ( ‘⟨𝑎, 𝑏⟩)
1413fveq2i 6151 . . . . . . 7 (𝐹‘(𝑎 𝑏)) = (𝐹‘( ‘⟨𝑎, 𝑏⟩))
1511, 12, 143eqtr4g 2680 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(𝐹 )𝑏) = (𝐹‘(𝑎 𝑏)))
1615eqeq1d 2623 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹 )𝑏) = 0 ↔ (𝐹‘(𝑎 𝑏)) = 0))
173, 4grpsubcl 17416 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑏𝑋) → (𝑎 𝑏) ∈ 𝑋)
18173expb 1263 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎 𝑏) ∈ 𝑋)
192, 18sylan 488 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎 𝑏) ∈ 𝑋)
20 nrmmetd.1 . . . . . . . 8 ((𝜑𝑥𝑋) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
2120ralrimiva 2960 . . . . . . 7 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
22 fveq2 6148 . . . . . . . . . 10 (𝑥 = (𝑎 𝑏) → (𝐹𝑥) = (𝐹‘(𝑎 𝑏)))
2322eqeq1d 2623 . . . . . . . . 9 (𝑥 = (𝑎 𝑏) → ((𝐹𝑥) = 0 ↔ (𝐹‘(𝑎 𝑏)) = 0))
24 eqeq1 2625 . . . . . . . . 9 (𝑥 = (𝑎 𝑏) → (𝑥 = 0 ↔ (𝑎 𝑏) = 0 ))
2523, 24bibi12d 335 . . . . . . . 8 (𝑥 = (𝑎 𝑏) → (((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 )))
2625rspccva 3294 . . . . . . 7 ((∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑎 𝑏) ∈ 𝑋) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
2721, 26sylan 488 . . . . . 6 ((𝜑 ∧ (𝑎 𝑏) ∈ 𝑋) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
2819, 27syldan 487 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹‘(𝑎 𝑏)) = 0 ↔ (𝑎 𝑏) = 0 ))
29 nrmmetd.z . . . . . . . 8 0 = (0g𝐺)
303, 29, 4grpsubeq0 17422 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑏𝑋) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
31303expb 1263 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
322, 31sylan 488 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎 𝑏) = 0𝑎 = 𝑏))
3316, 28, 323bitrd 294 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏))
341adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝐹:𝑋⟶ℝ)
3519adantrr 752 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎 𝑏) ∈ 𝑋)
3634, 35ffvelrnd 6316 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ∈ ℝ)
372adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝐺 ∈ Grp)
38 simprll 801 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑎𝑋)
39 simprr 795 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑐𝑋)
403, 4grpsubcl 17416 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑎𝑋𝑐𝑋) → (𝑎 𝑐) ∈ 𝑋)
4137, 38, 39, 40syl3anc 1323 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎 𝑐) ∈ 𝑋)
4234, 41ffvelrnd 6316 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ∈ ℝ)
43 simprlr 802 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → 𝑏𝑋)
443, 4grpsubcl 17416 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 𝑐) ∈ 𝑋)
4537, 43, 39, 44syl3anc 1323 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑏 𝑐) ∈ 𝑋)
4634, 45ffvelrnd 6316 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ∈ ℝ)
4742, 46readdcld 10013 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))) ∈ ℝ)
483, 4grpsubcl 17416 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑎𝑋) → (𝑐 𝑎) ∈ 𝑋)
4937, 39, 38, 48syl3anc 1323 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐 𝑎) ∈ 𝑋)
5034, 49ffvelrnd 6316 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑐 𝑎)) ∈ ℝ)
513, 4grpsubcl 17416 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑏𝑋) → (𝑐 𝑏) ∈ 𝑋)
5237, 39, 43, 51syl3anc 1323 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐 𝑏) ∈ 𝑋)
5334, 52ffvelrnd 6316 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑐 𝑏)) ∈ ℝ)
5450, 53readdcld 10013 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))) ∈ ℝ)
553, 4grpnnncan2 17433 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝑎 𝑐) (𝑏 𝑐)) = (𝑎 𝑏))
5637, 38, 43, 39, 55syl13anc 1325 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝑎 𝑐) (𝑏 𝑐)) = (𝑎 𝑏))
5756fveq2d 6152 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) = (𝐹‘(𝑎 𝑏)))
58 nrmmetd.2 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
5958ralrimivva 2965 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
6059adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
61 oveq1 6611 . . . . . . . . . . . . 13 (𝑥 = (𝑎 𝑐) → (𝑥 𝑦) = ((𝑎 𝑐) 𝑦))
6261fveq2d 6152 . . . . . . . . . . . 12 (𝑥 = (𝑎 𝑐) → (𝐹‘(𝑥 𝑦)) = (𝐹‘((𝑎 𝑐) 𝑦)))
63 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = (𝑎 𝑐) → (𝐹𝑥) = (𝐹‘(𝑎 𝑐)))
6463oveq1d 6619 . . . . . . . . . . . 12 (𝑥 = (𝑎 𝑐) → ((𝐹𝑥) + (𝐹𝑦)) = ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)))
6562, 64breq12d 4626 . . . . . . . . . . 11 (𝑥 = (𝑎 𝑐) → ((𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)) ↔ (𝐹‘((𝑎 𝑐) 𝑦)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦))))
66 oveq2 6612 . . . . . . . . . . . . 13 (𝑦 = (𝑏 𝑐) → ((𝑎 𝑐) 𝑦) = ((𝑎 𝑐) (𝑏 𝑐)))
6766fveq2d 6152 . . . . . . . . . . . 12 (𝑦 = (𝑏 𝑐) → (𝐹‘((𝑎 𝑐) 𝑦)) = (𝐹‘((𝑎 𝑐) (𝑏 𝑐))))
68 fveq2 6148 . . . . . . . . . . . . 13 (𝑦 = (𝑏 𝑐) → (𝐹𝑦) = (𝐹‘(𝑏 𝑐)))
6968oveq2d 6620 . . . . . . . . . . . 12 (𝑦 = (𝑏 𝑐) → ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)) = ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7067, 69breq12d 4626 . . . . . . . . . . 11 (𝑦 = (𝑏 𝑐) → ((𝐹‘((𝑎 𝑐) 𝑦)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹𝑦)) ↔ (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐)))))
7165, 70rspc2va 3307 . . . . . . . . . 10 ((((𝑎 𝑐) ∈ 𝑋 ∧ (𝑏 𝑐) ∈ 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦))) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7241, 45, 60, 71syl21anc 1322 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘((𝑎 𝑐) (𝑏 𝑐))) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
7357, 72eqbrtrrd 4637 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))))
74 eleq1 2686 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑏𝑋𝑐𝑋))
7574anbi2d 739 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → ((𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑐𝑋)))
7675anbi2d 739 . . . . . . . . . . . 12 (𝑏 = 𝑐 → ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) ↔ (𝜑 ∧ (𝑎𝑋𝑐𝑋))))
77 oveq2 6612 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑎 𝑏) = (𝑎 𝑐))
7877fveq2d 6152 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝐹‘(𝑎 𝑏)) = (𝐹‘(𝑎 𝑐)))
79 oveq1 6611 . . . . . . . . . . . . . 14 (𝑏 = 𝑐 → (𝑏 𝑎) = (𝑐 𝑎))
8079fveq2d 6152 . . . . . . . . . . . . 13 (𝑏 = 𝑐 → (𝐹‘(𝑏 𝑎)) = (𝐹‘(𝑐 𝑎)))
8178, 80breq12d 4626 . . . . . . . . . . . 12 (𝑏 = 𝑐 → ((𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎)) ↔ (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎))))
8276, 81imbi12d 334 . . . . . . . . . . 11 (𝑏 = 𝑐 → (((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎))) ↔ ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))))
832adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝐺 ∈ Grp)
843, 29grpidcl 17371 . . . . . . . . . . . . . 14 (𝐺 ∈ Grp → 0𝑋)
8583, 84syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 0𝑋)
86 simprr 795 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝑏𝑋)
87 simprl 793 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝑎𝑋)
883, 4grpsubcl 17416 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑎𝑋) → (𝑏 𝑎) ∈ 𝑋)
8983, 86, 87, 88syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑏 𝑎) ∈ 𝑋)
9059adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)))
91 oveq1 6611 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑥 𝑦) = ( 0 𝑦))
9291fveq2d 6152 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (𝐹‘(𝑥 𝑦)) = (𝐹‘( 0 𝑦)))
93 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝐹𝑥) = (𝐹0 ))
9493oveq1d 6619 . . . . . . . . . . . . . . 15 (𝑥 = 0 → ((𝐹𝑥) + (𝐹𝑦)) = ((𝐹0 ) + (𝐹𝑦)))
9592, 94breq12d 4626 . . . . . . . . . . . . . 14 (𝑥 = 0 → ((𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦)) ↔ (𝐹‘( 0 𝑦)) ≤ ((𝐹0 ) + (𝐹𝑦))))
96 oveq2 6612 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏 𝑎) → ( 0 𝑦) = ( 0 (𝑏 𝑎)))
9796fveq2d 6152 . . . . . . . . . . . . . . 15 (𝑦 = (𝑏 𝑎) → (𝐹‘( 0 𝑦)) = (𝐹‘( 0 (𝑏 𝑎))))
98 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑏 𝑎) → (𝐹𝑦) = (𝐹‘(𝑏 𝑎)))
9998oveq2d 6620 . . . . . . . . . . . . . . 15 (𝑦 = (𝑏 𝑎) → ((𝐹0 ) + (𝐹𝑦)) = ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
10097, 99breq12d 4626 . . . . . . . . . . . . . 14 (𝑦 = (𝑏 𝑎) → ((𝐹‘( 0 𝑦)) ≤ ((𝐹0 ) + (𝐹𝑦)) ↔ (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎)))))
10195, 100rspc2va 3307 . . . . . . . . . . . . 13 ((( 0𝑋 ∧ (𝑏 𝑎) ∈ 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝐹‘(𝑥 𝑦)) ≤ ((𝐹𝑥) + (𝐹𝑦))) → (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
10285, 89, 90, 101syl21anc 1322 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘( 0 (𝑏 𝑎))) ≤ ((𝐹0 ) + (𝐹‘(𝑏 𝑎))))
103 eqid 2621 . . . . . . . . . . . . . . . 16 (invg𝐺) = (invg𝐺)
1043, 4, 103, 29grpinvval2 17419 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (𝑏 𝑎) ∈ 𝑋) → ((invg𝐺)‘(𝑏 𝑎)) = ( 0 (𝑏 𝑎)))
10583, 89, 104syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((invg𝐺)‘(𝑏 𝑎)) = ( 0 (𝑏 𝑎)))
1063, 4, 103grpinvsub 17418 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑎𝑋) → ((invg𝐺)‘(𝑏 𝑎)) = (𝑎 𝑏))
10783, 86, 87, 106syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((invg𝐺)‘(𝑏 𝑎)) = (𝑎 𝑏))
108105, 107eqtr3d 2657 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ( 0 (𝑏 𝑎)) = (𝑎 𝑏))
109108fveq2d 6152 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘( 0 (𝑏 𝑎))) = (𝐹‘(𝑎 𝑏)))
1102, 84syl 17 . . . . . . . . . . . . . . . 16 (𝜑0𝑋)
111 pm5.501 356 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ (𝑥 = 0 ↔ (𝐹𝑥) = 0)))
112 bicom 212 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 0 ↔ (𝐹𝑥) = 0) ↔ ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ))
113111, 112syl6bb 276 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ ((𝐹𝑥) = 0 ↔ 𝑥 = 0 )))
11493eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → ((𝐹𝑥) = 0 ↔ (𝐹0 ) = 0))
115113, 114bitr3d 270 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (𝐹0 ) = 0))
116115rspccva 3294 . . . . . . . . . . . . . . . 16 ((∀𝑥𝑋 ((𝐹𝑥) = 0 ↔ 𝑥 = 0 ) ∧ 0𝑋) → (𝐹0 ) = 0)
11721, 110, 116syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹0 ) = 0)
118117adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹0 ) = 0)
119118oveq1d 6619 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹0 ) + (𝐹‘(𝑏 𝑎))) = (0 + (𝐹‘(𝑏 𝑎))))
1201adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → 𝐹:𝑋⟶ℝ)
121120, 89ffvelrnd 6316 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑏 𝑎)) ∈ ℝ)
122121recnd 10012 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑏 𝑎)) ∈ ℂ)
123122addid2d 10181 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (0 + (𝐹‘(𝑏 𝑎))) = (𝐹‘(𝑏 𝑎)))
124119, 123eqtrd 2655 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹0 ) + (𝐹‘(𝑏 𝑎))) = (𝐹‘(𝑏 𝑎)))
125102, 109, 1243brtr3d 4644 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ (𝐹‘(𝑏 𝑎)))
12682, 125chvarv 2262 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))
127126adantrlr 758 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)))
128 eleq1 2686 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑎𝑋𝑏𝑋))
129128anbi1d 740 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → ((𝑎𝑋𝑐𝑋) ↔ (𝑏𝑋𝑐𝑋)))
130129anbi2d 739 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ((𝜑 ∧ (𝑎𝑋𝑐𝑋)) ↔ (𝜑 ∧ (𝑏𝑋𝑐𝑋))))
131 oveq1 6611 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑎 𝑐) = (𝑏 𝑐))
132131fveq2d 6152 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → (𝐹‘(𝑎 𝑐)) = (𝐹‘(𝑏 𝑐)))
133 oveq2 6612 . . . . . . . . . . . . . 14 (𝑎 = 𝑏 → (𝑐 𝑎) = (𝑐 𝑏))
134133fveq2d 6152 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → (𝐹‘(𝑐 𝑎)) = (𝐹‘(𝑐 𝑏)))
135132, 134breq12d 4626 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ((𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎)) ↔ (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏))))
136130, 135imbi12d 334 . . . . . . . . . . 11 (𝑎 = 𝑏 → (((𝜑 ∧ (𝑎𝑋𝑐𝑋)) → (𝐹‘(𝑎 𝑐)) ≤ (𝐹‘(𝑐 𝑎))) ↔ ((𝜑 ∧ (𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))))
137136, 126chvarv 2262 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))
138137adantrll 757 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑏 𝑐)) ≤ (𝐹‘(𝑐 𝑏)))
13942, 46, 50, 53, 127, 138le2addd 10590 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹‘(𝑎 𝑐)) + (𝐹‘(𝑏 𝑐))) ≤ ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
14036, 47, 54, 73, 139letrd 10138 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝐹‘(𝑎 𝑏)) ≤ ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
14115adantrr 752 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎(𝐹 )𝑏) = (𝐹‘(𝑎 𝑏)))
1426adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → :(𝑋 × 𝑋)⟶𝑋)
143 opelxpi 5108 . . . . . . . . . . 11 ((𝑐𝑋𝑎𝑋) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
14439, 38, 143syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
145 fvco3 6232 . . . . . . . . . 10 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑐, 𝑎⟩) = (𝐹‘( ‘⟨𝑐, 𝑎⟩)))
146142, 144, 145syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹 )‘⟨𝑐, 𝑎⟩) = (𝐹‘( ‘⟨𝑐, 𝑎⟩)))
147 df-ov 6607 . . . . . . . . 9 (𝑐(𝐹 )𝑎) = ((𝐹 )‘⟨𝑐, 𝑎⟩)
148 df-ov 6607 . . . . . . . . . 10 (𝑐 𝑎) = ( ‘⟨𝑐, 𝑎⟩)
149148fveq2i 6151 . . . . . . . . 9 (𝐹‘(𝑐 𝑎)) = (𝐹‘( ‘⟨𝑐, 𝑎⟩))
150146, 147, 1493eqtr4g 2680 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐(𝐹 )𝑎) = (𝐹‘(𝑐 𝑎)))
151 opelxpi 5108 . . . . . . . . . . 11 ((𝑐𝑋𝑏𝑋) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
15239, 43, 151syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
153 fvco3 6232 . . . . . . . . . 10 (( :(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 )‘⟨𝑐, 𝑏⟩) = (𝐹‘( ‘⟨𝑐, 𝑏⟩)))
154142, 152, 153syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝐹 )‘⟨𝑐, 𝑏⟩) = (𝐹‘( ‘⟨𝑐, 𝑏⟩)))
155 df-ov 6607 . . . . . . . . 9 (𝑐(𝐹 )𝑏) = ((𝐹 )‘⟨𝑐, 𝑏⟩)
156 df-ov 6607 . . . . . . . . . 10 (𝑐 𝑏) = ( ‘⟨𝑐, 𝑏⟩)
157156fveq2i 6151 . . . . . . . . 9 (𝐹‘(𝑐 𝑏)) = (𝐹‘( ‘⟨𝑐, 𝑏⟩))
158154, 155, 1573eqtr4g 2680 . . . . . . . 8 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑐(𝐹 )𝑏) = (𝐹‘(𝑐 𝑏)))
159150, 158oveq12d 6622 . . . . . . 7 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)) = ((𝐹‘(𝑐 𝑎)) + (𝐹‘(𝑐 𝑏))))
160140, 141, 1593brtr4d 4645 . . . . . 6 ((𝜑 ∧ ((𝑎𝑋𝑏𝑋) ∧ 𝑐𝑋)) → (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))
161160expr 642 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑐𝑋 → (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
162161ralrimiv 2959 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))
16333, 162jca 554 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
164163ralrimivva 2965 . 2 (𝜑 → ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))
165 fvex 6158 . . . 4 (Base‘𝐺) ∈ V
1663, 165eqeltri 2694 . . 3 𝑋 ∈ V
167 ismet 22038 . . 3 (𝑋 ∈ V → ((𝐹 ) ∈ (Met‘𝑋) ↔ ((𝐹 ):(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏))))))
168166, 167ax-mp 5 . 2 ((𝐹 ) ∈ (Met‘𝑋) ↔ ((𝐹 ):(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑎𝑋𝑏𝑋 (((𝑎(𝐹 )𝑏) = 0 ↔ 𝑎 = 𝑏) ∧ ∀𝑐𝑋 (𝑎(𝐹 )𝑏) ≤ ((𝑐(𝐹 )𝑎) + (𝑐(𝐹 )𝑏)))))
1698, 164, 168sylanbrc 697 1 (𝜑 → (𝐹 ) ∈ (Met‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  cop 4154   class class class wbr 4613   × cxp 5072  ccom 5078  wf 5843  cfv 5847  (class class class)co 6604  cr 9879  0cc0 9880   + caddc 9883  cle 10019  Basecbs 15781  0gc0g 16021  Grpcgrp 17343  invgcminusg 17344  -gcsg 17345  Metcme 19651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-po 4995  df-so 4996  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-1st 7113  df-2nd 7114  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-0g 16023  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-grp 17346  df-minusg 17347  df-sbg 17348  df-met 19659
This theorem is referenced by:  abvmet  22290  tngngpd  22367
  Copyright terms: Public domain W3C validator