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

Theorem tngngp3 22739
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‘𝐺)
21fvexi 6389 . . . 4 𝑋 ∈ V
3 fex 6682 . . . 4 ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V)
42, 3mpan2 682 . . 3 (𝑁:𝑋⟶ℝ → 𝑁 ∈ V)
5 tngngp3.t . . . . . . 7 𝑇 = (𝐺 toNrmGrp 𝑁)
65tnggrpr 22738 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
7 simp2 1167 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp)
8 eqid 2765 . . . . . . . . . . . . . 14 (Base‘𝑇) = (Base‘𝑇)
9 eqid 2765 . . . . . . . . . . . . . 14 (norm‘𝑇) = (norm‘𝑇)
10 eqid 2765 . . . . . . . . . . . . . 14 (0g𝑇) = (0g𝑇)
118, 9, 10nmeq0 22701 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)))
12 eqid 2765 . . . . . . . . . . . . . 14 (invg𝑇) = (invg𝑇)
138, 9, 12nminv 22704 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))
14 eqid 2765 . . . . . . . . . . . . . . . 16 (+g𝑇) = (+g𝑇)
158, 9, 14nmtri 22709 . . . . . . . . . . . . . . 15 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
16153expa 1147 . . . . . . . . . . . . . 14 (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1716ralrimiva 3113 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1811, 13, 173jca 1158 . . . . . . . . . . . 12 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
1918ralrimiva 3113 . . . . . . . . . . 11 (𝑇 ∈ NrmGrp → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2019adantl 473 . . . . . . . . . 10 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
21203ad2ant1 1163 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
225, 1tngbas 22724 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝑋 = (Base‘𝑇))
23 tngngp3.p . . . . . . . . . . . . . . 15 + = (+g𝐺)
245, 23tngplusg 22725 . . . . . . . . . . . . . 14 (𝑁 ∈ V → + = (+g𝑇))
25 tngngp3.i . . . . . . . . . . . . . . 15 𝐼 = (invg𝐺)
26 eqidd 2766 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝐺))
27 eqid 2765 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) = (Base‘𝐺)
285, 27tngbas 22724 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝑇))
29 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (+g𝐺) = (+g𝐺)
305, 29tngplusg 22725 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ V → (+g𝐺) = (+g𝑇))
3130oveqd 6859 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ V → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3231adantr 472 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3326, 28, 32grpinvpropd 17757 . . . . . . . . . . . . . . 15 (𝑁 ∈ V → (invg𝐺) = (invg𝑇))
3425, 33syl5eq 2811 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝐼 = (invg𝑇))
3522, 24, 343jca 1158 . . . . . . . . . . . . 13 (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
3635adantr 472 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
37363ad2ant1 1163 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
38 reex 10280 . . . . . . . . . . . . 13 ℝ ∈ V
395, 1, 38tngnm 22734 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
40393adant1 1160 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
41 tngngp3.z . . . . . . . . . . . . . 14 0 = (0g𝐺)
425, 41tng0 22726 . . . . . . . . . . . . 13 (𝑁 ∈ V → 0 = (0g𝑇))
4342adantr 472 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 = (0g𝑇))
44433ad2ant1 1163 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 = (0g𝑇))
4537, 40, 443jca 1158 . . . . . . . . . 10 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)))
46 simp1 1166 . . . . . . . . . . . 12 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝑋 = (Base‘𝑇))
47463ad2ant1 1163 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑋 = (Base‘𝑇))
48 simp2 1167 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑁 = (norm‘𝑇))
4948fveq1d 6377 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
5049eqeq1d 2767 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0))
51 simp3 1168 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 0 = (0g𝑇))
5251eqeq2d 2775 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 = 0𝑥 = (0g𝑇)))
5350, 52bibi12d 336 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇))))
54 simp3 1168 . . . . . . . . . . . . . . . 16 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝐼 = (invg𝑇))
55543ad2ant1 1163 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝐼 = (invg𝑇))
5655fveq1d 6377 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝐼𝑥) = ((invg𝑇)‘𝑥))
5748, 56fveq12d 6382 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝐼𝑥)) = ((norm‘𝑇)‘((invg𝑇)‘𝑥)))
5857, 49eqeq12d 2780 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)))
59 simp2 1167 . . . . . . . . . . . . . . . . 17 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → + = (+g𝑇))
60593ad2ant1 1163 . . . . . . . . . . . . . . . 16 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → + = (+g𝑇))
6160oveqd 6859 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 + 𝑦) = (𝑥(+g𝑇)𝑦))
6248, 61fveq12d 6382 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)))
63 fveq1 6374 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
64 fveq1 6374 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑦) = ((norm‘𝑇)‘𝑦))
6563, 64oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑁 = (norm‘𝑇) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
66653ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
6762, 66breq12d 4822 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6847, 67raleqbidv 3300 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6953, 58, 683anbi123d 1560 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7047, 69raleqbidv 3300 . . . . . . . . . 10 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7145, 70syl 17 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7221, 71mpbird 248 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
737, 72jca 507 . . . . . . 7 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
74733exp 1148 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
756, 74mpd 15 . . . . 5 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
7675expcom 402 . . . 4 (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
7776com13 88 . . 3 (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
784, 77mpd 15 . 2 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
79 eqid 2765 . . . 4 (-g𝐺) = (-g𝐺)
80 simpl 474 . . . . 5 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝐺 ∈ Grp)
8180adantl 473 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝐺 ∈ Grp)
82 simpl 474 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑁:𝑋⟶ℝ)
83 fveq2 6375 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁𝑥) = (𝑁𝑎))
8483eqeq1d 2767 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁𝑥) = 0 ↔ (𝑁𝑎) = 0))
85 eqeq1 2769 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥 = 0𝑎 = 0 ))
8684, 85bibi12d 336 . . . . . . . . . . 11 (𝑥 = 𝑎 → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
87 fveq2 6375 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝐼𝑥) = (𝐼𝑎))
8887fveq2d 6379 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑎)))
8988, 83eqeq12d 2780 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑎)) = (𝑁𝑎)))
90 fvoveq1 6865 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦)))
9183oveq1d 6857 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝑁𝑥) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁𝑦)))
9290, 91breq12d 4822 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9392ralbidv 3133 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9486, 89, 933anbi123d 1560 . . . . . . . . . 10 (𝑥 = 𝑎 → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)))))
9594rspccva 3460 . . . . . . . . 9 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
96 simp1 1166 . . . . . . . . 9 ((((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9795, 96syl 17 . . . . . . . 8 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9897ex 401 . . . . . . 7 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
9998adantl 473 . . . . . 6 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
10099adantl 473 . . . . 5 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
101100imp 395 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
1021, 23, 25, 79grpsubval 17732 . . . . . . 7 ((𝑎𝑋𝑏𝑋) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
103102adantl 473 . . . . . 6 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
104103fveq2d 6379 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼𝑏))))
105 3simpc 1182 . . . . . . . . . 10 ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
106105ralimi 3099 . . . . . . . . 9 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
107 simpr 477 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
108107ralimi 3099 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
109 oveq2 6850 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼𝑏)))
110109fveq2d 6379 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼𝑏))))
111 fveq2 6375 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑁𝑦) = (𝑁‘(𝐼𝑏)))
112111oveq2d 6858 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → ((𝑁𝑎) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
113110, 112breq12d 4822 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐼𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
11492, 113rspc2v 3474 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋) → (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
1151, 25grpinvcl 17734 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝑏𝑋) → (𝐼𝑏) ∈ 𝑋)
116115ex 401 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ Grp → (𝑏𝑋 → (𝐼𝑏) ∈ 𝑋))
117116anim2d 605 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋)))
118117imp 395 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋))
119114, 118syl11 33 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
120119expd 404 . . . . . . . . . . . . . . 15 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
121108, 120syl 17 . . . . . . . . . . . . . 14 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
122121imp 395 . . . . . . . . . . . . 13 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
123122imp 395 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
124 simpl 474 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
125124ralimi 3099 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
126 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐼𝑥) = (𝐼𝑏))
127126fveq2d 6379 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑏)))
128 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁𝑥) = (𝑁𝑏))
129127, 128eqeq12d 2780 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑏)) = (𝑁𝑏)))
130129rspccva 3460 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁‘(𝐼𝑏)) = (𝑁𝑏))
131130eqcomd 2771 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
132131ex 401 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
133125, 132syl 17 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
134133adantr 472 . . . . . . . . . . . . . . 15 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
135134adantld 484 . . . . . . . . . . . . . 14 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
136135imp 395 . . . . . . . . . . . . 13 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
137136oveq2d 6858 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑁𝑎) + (𝑁𝑏)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
138123, 137breqtrrd 4837 . . . . . . . . . . 11 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
139138ex 401 . . . . . . . . . 10 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
140139ex 401 . . . . . . . . 9 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
141106, 140syl 17 . . . . . . . 8 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
142141impcom 396 . . . . . . 7 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
143142adantl 473 . . . . . 6 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
144143imp 395 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
145104, 144eqbrtrd 4831 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) ≤ ((𝑁𝑎) + (𝑁𝑏)))
1465, 1, 79, 41, 81, 82, 101, 145tngngpd 22736 . . 3 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑇 ∈ NrmGrp)
147146ex 401 . 2 (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝑇 ∈ NrmGrp))
14878, 147impbid 203 1 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  cr 10188  0cc0 10189   + caddc 10192  cle 10329  Basecbs 16130  +gcplusg 16214  0gc0g 16366  Grpcgrp 17689  invgcminusg 17690  -gcsg 17691  normcnm 22660  NrmGrpcngp 22661   toNrmGrp ctng 22662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-plusg 16227  df-tset 16233  df-ds 16236  df-rest 16349  df-topn 16350  df-0g 16368  df-topgen 16370  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-grp 17692  df-minusg 17693  df-sbg 17694  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-xms 22404  df-ms 22405  df-nm 22666  df-ngp 22667  df-tng 22668
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator