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

Theorem tngngp3 22507
Description: Alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021.)
Hypotheses
Ref Expression
tngngp3.t 𝑇 = (𝐺 toNrmGrp 𝑁)
tngngp3.x 𝑋 = (Base‘𝐺)
tngngp3.z 0 = (0g𝐺)
tngngp3.p + = (+g𝐺)
tngngp3.i 𝐼 = (invg𝐺)
Assertion
Ref Expression
tngngp3 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Distinct variable groups:   𝑥,𝐺,𝑦   𝑥,𝑁,𝑦   𝑥,𝑇,𝑦   𝑥,𝑋,𝑦   𝑥,𝐼,𝑦   𝑥, + ,𝑦   𝑥, 0 ,𝑦

Proof of Theorem tngngp3
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tngngp3.x . . . . 5 𝑋 = (Base‘𝐺)
2 fvex 6239 . . . . 5 (Base‘𝐺) ∈ V
31, 2eqeltri 2726 . . . 4 𝑋 ∈ V
4 fex 6530 . . . 4 ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V)
53, 4mpan2 707 . . 3 (𝑁:𝑋⟶ℝ → 𝑁 ∈ V)
6 tngngp3.t . . . . . . 7 𝑇 = (𝐺 toNrmGrp 𝑁)
76tnggrpr 22506 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
8 simp2 1082 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp)
9 eqid 2651 . . . . . . . . . . . . . 14 (Base‘𝑇) = (Base‘𝑇)
10 eqid 2651 . . . . . . . . . . . . . 14 (norm‘𝑇) = (norm‘𝑇)
11 eqid 2651 . . . . . . . . . . . . . 14 (0g𝑇) = (0g𝑇)
129, 10, 11nmeq0 22469 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)))
13 eqid 2651 . . . . . . . . . . . . . 14 (invg𝑇) = (invg𝑇)
149, 10, 13nminv 22472 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))
15 eqid 2651 . . . . . . . . . . . . . . . 16 (+g𝑇) = (+g𝑇)
169, 10, 15nmtri 22477 . . . . . . . . . . . . . . 15 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
17163expa 1284 . . . . . . . . . . . . . 14 (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1817ralrimiva 2995 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1912, 14, 183jca 1261 . . . . . . . . . . . 12 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2019ralrimiva 2995 . . . . . . . . . . 11 (𝑇 ∈ NrmGrp → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2120adantl 481 . . . . . . . . . 10 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
22213ad2ant1 1102 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
236, 1tngbas 22492 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝑋 = (Base‘𝑇))
24 tngngp3.p . . . . . . . . . . . . . . 15 + = (+g𝐺)
256, 24tngplusg 22493 . . . . . . . . . . . . . 14 (𝑁 ∈ V → + = (+g𝑇))
26 tngngp3.i . . . . . . . . . . . . . . 15 𝐼 = (invg𝐺)
27 eqidd 2652 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝐺))
28 eqid 2651 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) = (Base‘𝐺)
296, 28tngbas 22492 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝑇))
30 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (+g𝐺) = (+g𝐺)
316, 30tngplusg 22493 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ V → (+g𝐺) = (+g𝑇))
3231oveqd 6707 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ V → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3332adantr 480 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3427, 29, 33grpinvpropd 17537 . . . . . . . . . . . . . . 15 (𝑁 ∈ V → (invg𝐺) = (invg𝑇))
3526, 34syl5eq 2697 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝐼 = (invg𝑇))
3623, 25, 353jca 1261 . . . . . . . . . . . . 13 (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
3736adantr 480 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
38373ad2ant1 1102 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
39 reex 10065 . . . . . . . . . . . . 13 ℝ ∈ V
406, 1, 39tngnm 22502 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
41403adant1 1099 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
42 tngngp3.z . . . . . . . . . . . . . 14 0 = (0g𝐺)
436, 42tng0 22494 . . . . . . . . . . . . 13 (𝑁 ∈ V → 0 = (0g𝑇))
4443adantr 480 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 = (0g𝑇))
45443ad2ant1 1102 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 = (0g𝑇))
4638, 41, 453jca 1261 . . . . . . . . . 10 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)))
47 simp1 1081 . . . . . . . . . . . 12 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝑋 = (Base‘𝑇))
48473ad2ant1 1102 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑋 = (Base‘𝑇))
49 simp2 1082 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑁 = (norm‘𝑇))
5049fveq1d 6231 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
5150eqeq1d 2653 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0))
52 simp3 1083 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 0 = (0g𝑇))
5352eqeq2d 2661 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 = 0𝑥 = (0g𝑇)))
5451, 53bibi12d 334 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇))))
55 simp3 1083 . . . . . . . . . . . . . . . 16 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝐼 = (invg𝑇))
56553ad2ant1 1102 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝐼 = (invg𝑇))
5756fveq1d 6231 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝐼𝑥) = ((invg𝑇)‘𝑥))
5849, 57fveq12d 6235 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝐼𝑥)) = ((norm‘𝑇)‘((invg𝑇)‘𝑥)))
5958, 50eqeq12d 2666 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)))
60 simp2 1082 . . . . . . . . . . . . . . . . 17 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → + = (+g𝑇))
61603ad2ant1 1102 . . . . . . . . . . . . . . . 16 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → + = (+g𝑇))
6261oveqd 6707 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 + 𝑦) = (𝑥(+g𝑇)𝑦))
6349, 62fveq12d 6235 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)))
64 fveq1 6228 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
65 fveq1 6228 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑦) = ((norm‘𝑇)‘𝑦))
6664, 65oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑁 = (norm‘𝑇) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
67663ad2ant2 1103 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
6863, 67breq12d 4698 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6948, 68raleqbidv 3182 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
7054, 59, 693anbi123d 1439 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7148, 70raleqbidv 3182 . . . . . . . . . 10 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7246, 71syl 17 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7322, 72mpbird 247 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
748, 73jca 553 . . . . . . 7 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
75743exp 1283 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
767, 75mpd 15 . . . . 5 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
7776expcom 450 . . . 4 (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
7877com13 88 . . 3 (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
795, 78mpd 15 . 2 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
80 eqid 2651 . . . 4 (-g𝐺) = (-g𝐺)
81 simpl 472 . . . . 5 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝐺 ∈ Grp)
8281adantl 481 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝐺 ∈ Grp)
83 simpl 472 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑁:𝑋⟶ℝ)
84 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁𝑥) = (𝑁𝑎))
8584eqeq1d 2653 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁𝑥) = 0 ↔ (𝑁𝑎) = 0))
86 eqeq1 2655 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥 = 0𝑎 = 0 ))
8785, 86bibi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑎 → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
88 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝐼𝑥) = (𝐼𝑎))
8988fveq2d 6233 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑎)))
9089, 84eqeq12d 2666 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑎)) = (𝑁𝑎)))
91 oveq1 6697 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦))
9291fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦)))
9384oveq1d 6705 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝑁𝑥) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁𝑦)))
9492, 93breq12d 4698 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9594ralbidv 3015 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9687, 90, 953anbi123d 1439 . . . . . . . . . 10 (𝑥 = 𝑎 → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)))))
9796rspccva 3339 . . . . . . . . 9 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
98 simp1 1081 . . . . . . . . 9 ((((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9997, 98syl 17 . . . . . . . 8 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
10099ex 449 . . . . . . 7 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
101100adantl 481 . . . . . 6 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
102101adantl 481 . . . . 5 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
103102imp 444 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
1041, 24, 26, 80grpsubval 17512 . . . . . . 7 ((𝑎𝑋𝑏𝑋) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
105104adantl 481 . . . . . 6 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
106105fveq2d 6233 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼𝑏))))
107 3simpc 1080 . . . . . . . . . 10 ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
108107ralimi 2981 . . . . . . . . 9 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
109 simpr 476 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
110109ralimi 2981 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
111 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼𝑏)))
112111fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼𝑏))))
113 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑁𝑦) = (𝑁‘(𝐼𝑏)))
114113oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → ((𝑁𝑎) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
115112, 114breq12d 4698 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐼𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
11694, 115rspc2v 3353 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋) → (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
1171, 26grpinvcl 17514 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝑏𝑋) → (𝐼𝑏) ∈ 𝑋)
118117ex 449 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ Grp → (𝑏𝑋 → (𝐼𝑏) ∈ 𝑋))
119118anim2d 588 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋)))
120119imp 444 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋))
121116, 120syl11 33 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
122121expd 451 . . . . . . . . . . . . . . 15 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
123110, 122syl 17 . . . . . . . . . . . . . 14 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
124123imp 444 . . . . . . . . . . . . 13 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
125124imp 444 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
126 simpl 472 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
127126ralimi 2981 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
128 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐼𝑥) = (𝐼𝑏))
129128fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑏)))
130 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁𝑥) = (𝑁𝑏))
131129, 130eqeq12d 2666 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑏)) = (𝑁𝑏)))
132131rspccva 3339 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁‘(𝐼𝑏)) = (𝑁𝑏))
133132eqcomd 2657 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
134133ex 449 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
135127, 134syl 17 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
136135adantr 480 . . . . . . . . . . . . . . 15 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
137136adantld 482 . . . . . . . . . . . . . 14 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
138137imp 444 . . . . . . . . . . . . 13 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
139138oveq2d 6706 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑁𝑎) + (𝑁𝑏)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
140125, 139breqtrrd 4713 . . . . . . . . . . 11 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
141140ex 449 . . . . . . . . . 10 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
142141ex 449 . . . . . . . . 9 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
143108, 142syl 17 . . . . . . . 8 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
144143impcom 445 . . . . . . 7 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
145144adantl 481 . . . . . 6 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
146145imp 444 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
147106, 146eqbrtrd 4707 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) ≤ ((𝑁𝑎) + (𝑁𝑏)))
1486, 1, 80, 42, 82, 83, 103, 147tngngpd 22504 . . 3 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑇 ∈ NrmGrp)
149148ex 449 . 2 (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝑇 ∈ NrmGrp))
15079, 149impbid 202 1 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231   class class class wbr 4685  wf 5922  cfv 5926  (class class class)co 6690  cr 9973  0cc0 9974   + caddc 9977  cle 10113  Basecbs 15904  +gcplusg 15988  0gc0g 16147  Grpcgrp 17469  invgcminusg 17470  -gcsg 17471  normcnm 22428  NrmGrpcngp 22429   toNrmGrp ctng 22430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-plusg 16001  df-tset 16007  df-ds 16011  df-rest 16130  df-topn 16131  df-0g 16149  df-topgen 16151  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472  df-minusg 17473  df-sbg 17474  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-xms 22172  df-ms 22173  df-nm 22434  df-ngp 22435  df-tng 22436
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator