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

Theorem tngngp3 22680
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 6342 . . . . 5 (Base‘𝐺) ∈ V
31, 2eqeltri 2846 . . . 4 𝑋 ∈ V
4 fex 6633 . . . 4 ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V)
53, 4mpan2 671 . . 3 (𝑁:𝑋⟶ℝ → 𝑁 ∈ V)
6 tngngp3.t . . . . . . 7 𝑇 = (𝐺 toNrmGrp 𝑁)
76tnggrpr 22679 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
8 simp2 1131 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp)
9 eqid 2771 . . . . . . . . . . . . . 14 (Base‘𝑇) = (Base‘𝑇)
10 eqid 2771 . . . . . . . . . . . . . 14 (norm‘𝑇) = (norm‘𝑇)
11 eqid 2771 . . . . . . . . . . . . . 14 (0g𝑇) = (0g𝑇)
129, 10, 11nmeq0 22642 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)))
13 eqid 2771 . . . . . . . . . . . . . 14 (invg𝑇) = (invg𝑇)
149, 10, 13nminv 22645 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))
15 eqid 2771 . . . . . . . . . . . . . . . 16 (+g𝑇) = (+g𝑇)
169, 10, 15nmtri 22650 . . . . . . . . . . . . . . 15 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
17163expa 1111 . . . . . . . . . . . . . 14 (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1817ralrimiva 3115 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1912, 14, 183jca 1122 . . . . . . . . . . . 12 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2019ralrimiva 3115 . . . . . . . . . . 11 (𝑇 ∈ NrmGrp → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2120adantl 467 . . . . . . . . . 10 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
22213ad2ant1 1127 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
236, 1tngbas 22665 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝑋 = (Base‘𝑇))
24 tngngp3.p . . . . . . . . . . . . . . 15 + = (+g𝐺)
256, 24tngplusg 22666 . . . . . . . . . . . . . 14 (𝑁 ∈ V → + = (+g𝑇))
26 tngngp3.i . . . . . . . . . . . . . . 15 𝐼 = (invg𝐺)
27 eqidd 2772 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝐺))
28 eqid 2771 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) = (Base‘𝐺)
296, 28tngbas 22665 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝑇))
30 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (+g𝐺) = (+g𝐺)
316, 30tngplusg 22666 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ V → (+g𝐺) = (+g𝑇))
3231oveqd 6810 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ V → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3332adantr 466 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3427, 29, 33grpinvpropd 17698 . . . . . . . . . . . . . . 15 (𝑁 ∈ V → (invg𝐺) = (invg𝑇))
3526, 34syl5eq 2817 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝐼 = (invg𝑇))
3623, 25, 353jca 1122 . . . . . . . . . . . . 13 (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
3736adantr 466 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
38373ad2ant1 1127 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
39 reex 10229 . . . . . . . . . . . . 13 ℝ ∈ V
406, 1, 39tngnm 22675 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
41403adant1 1124 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
42 tngngp3.z . . . . . . . . . . . . . 14 0 = (0g𝐺)
436, 42tng0 22667 . . . . . . . . . . . . 13 (𝑁 ∈ V → 0 = (0g𝑇))
4443adantr 466 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 = (0g𝑇))
45443ad2ant1 1127 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 = (0g𝑇))
4638, 41, 453jca 1122 . . . . . . . . . 10 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)))
47 simp1 1130 . . . . . . . . . . . 12 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝑋 = (Base‘𝑇))
48473ad2ant1 1127 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑋 = (Base‘𝑇))
49 simp2 1131 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑁 = (norm‘𝑇))
5049fveq1d 6334 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
5150eqeq1d 2773 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0))
52 simp3 1132 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 0 = (0g𝑇))
5352eqeq2d 2781 . . . . . . . . . . . . 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 1132 . . . . . . . . . . . . . . . 16 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝐼 = (invg𝑇))
56553ad2ant1 1127 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝐼 = (invg𝑇))
5756fveq1d 6334 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝐼𝑥) = ((invg𝑇)‘𝑥))
5849, 57fveq12d 6338 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝐼𝑥)) = ((norm‘𝑇)‘((invg𝑇)‘𝑥)))
5958, 50eqeq12d 2786 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)))
60 simp2 1131 . . . . . . . . . . . . . . . . 17 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → + = (+g𝑇))
61603ad2ant1 1127 . . . . . . . . . . . . . . . 16 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → + = (+g𝑇))
6261oveqd 6810 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 + 𝑦) = (𝑥(+g𝑇)𝑦))
6349, 62fveq12d 6338 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)))
64 fveq1 6331 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
65 fveq1 6331 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑦) = ((norm‘𝑇)‘𝑦))
6664, 65oveq12d 6811 . . . . . . . . . . . . . . 15 (𝑁 = (norm‘𝑇) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
67663ad2ant2 1128 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
6863, 67breq12d 4799 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6948, 68raleqbidv 3301 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
7054, 59, 693anbi123d 1547 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7148, 70raleqbidv 3301 . . . . . . . . . 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 501 . . . . . . 7 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
75743exp 1112 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
767, 75mpd 15 . . . . 5 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
7776expcom 398 . . . 4 (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
7877com13 88 . . 3 (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
795, 78mpd 15 . 2 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
80 eqid 2771 . . . 4 (-g𝐺) = (-g𝐺)
81 simpl 468 . . . . 5 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝐺 ∈ Grp)
8281adantl 467 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝐺 ∈ Grp)
83 simpl 468 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑁:𝑋⟶ℝ)
84 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁𝑥) = (𝑁𝑎))
8584eqeq1d 2773 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁𝑥) = 0 ↔ (𝑁𝑎) = 0))
86 eqeq1 2775 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥 = 0𝑎 = 0 ))
8785, 86bibi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑎 → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
88 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝐼𝑥) = (𝐼𝑎))
8988fveq2d 6336 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑎)))
9089, 84eqeq12d 2786 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑎)) = (𝑁𝑎)))
91 fvoveq1 6816 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦)))
9284oveq1d 6808 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝑁𝑥) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁𝑦)))
9391, 92breq12d 4799 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9493ralbidv 3135 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9587, 90, 943anbi123d 1547 . . . . . . . . . 10 (𝑥 = 𝑎 → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)))))
9695rspccva 3459 . . . . . . . . 9 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
97 simp1 1130 . . . . . . . . 9 ((((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9896, 97syl 17 . . . . . . . 8 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9998ex 397 . . . . . . 7 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
10099adantl 467 . . . . . 6 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
101100adantl 467 . . . . 5 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
102101imp 393 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
1031, 24, 26, 80grpsubval 17673 . . . . . . 7 ((𝑎𝑋𝑏𝑋) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
104103adantl 467 . . . . . 6 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
105104fveq2d 6336 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼𝑏))))
106 3simpc 1146 . . . . . . . . . 10 ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
107106ralimi 3101 . . . . . . . . 9 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
108 simpr 471 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
109108ralimi 3101 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
110 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼𝑏)))
111110fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼𝑏))))
112 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑁𝑦) = (𝑁‘(𝐼𝑏)))
113112oveq2d 6809 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → ((𝑁𝑎) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
114111, 113breq12d 4799 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐼𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
11593, 114rspc2v 3472 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋) → (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
1161, 26grpinvcl 17675 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝑏𝑋) → (𝐼𝑏) ∈ 𝑋)
117116ex 397 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ Grp → (𝑏𝑋 → (𝐼𝑏) ∈ 𝑋))
118117anim2d 599 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋)))
119118imp 393 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋))
120115, 119syl11 33 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
121120expd 400 . . . . . . . . . . . . . . 15 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
122109, 121syl 17 . . . . . . . . . . . . . 14 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
123122imp 393 . . . . . . . . . . . . 13 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
124123imp 393 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
125 simpl 468 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
126125ralimi 3101 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
127 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐼𝑥) = (𝐼𝑏))
128127fveq2d 6336 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑏)))
129 fveq2 6332 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁𝑥) = (𝑁𝑏))
130128, 129eqeq12d 2786 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑏)) = (𝑁𝑏)))
131130rspccva 3459 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁‘(𝐼𝑏)) = (𝑁𝑏))
132131eqcomd 2777 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
133132ex 397 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
134126, 133syl 17 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
135134adantr 466 . . . . . . . . . . . . . . 15 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
136135adantld 478 . . . . . . . . . . . . . 14 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
137136imp 393 . . . . . . . . . . . . 13 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
138137oveq2d 6809 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑁𝑎) + (𝑁𝑏)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
139124, 138breqtrrd 4814 . . . . . . . . . . 11 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
140139ex 397 . . . . . . . . . 10 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
141140ex 397 . . . . . . . . 9 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
142107, 141syl 17 . . . . . . . 8 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
143142impcom 394 . . . . . . 7 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
144143adantl 467 . . . . . 6 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
145144imp 393 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
146105, 145eqbrtrd 4808 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) ≤ ((𝑁𝑎) + (𝑁𝑏)))
1476, 1, 80, 42, 82, 83, 102, 146tngngpd 22677 . . 3 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑇 ∈ NrmGrp)
148147ex 397 . 2 (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝑇 ∈ NrmGrp))
14979, 148impbid 202 1 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  Vcvv 3351   class class class wbr 4786  wf 6027  cfv 6031  (class class class)co 6793  cr 10137  0cc0 10138   + caddc 10141  cle 10277  Basecbs 16064  +gcplusg 16149  0gc0g 16308  Grpcgrp 17630  invgcminusg 17631  -gcsg 17632  normcnm 22601  NrmGrpcngp 22602   toNrmGrp ctng 22603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-plusg 16162  df-tset 16168  df-ds 16172  df-rest 16291  df-topn 16292  df-0g 16310  df-topgen 16312  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-grp 17633  df-minusg 17634  df-sbg 17635  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-xms 22345  df-ms 22346  df-nm 22607  df-ngp 22608  df-tng 22609
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator