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

Theorem tngngp3 23363
 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 6676 . . . 4 𝑋 ∈ V
3 fex 6985 . . . 4 ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V)
42, 3mpan2 690 . . 3 (𝑁:𝑋⟶ℝ → 𝑁 ∈ V)
5 tngngp3.t . . . . . . 7 𝑇 = (𝐺 toNrmGrp 𝑁)
65tnggrpr 23362 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
7 simp2 1134 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp)
8 eqid 2758 . . . . . . . . . . . . . 14 (Base‘𝑇) = (Base‘𝑇)
9 eqid 2758 . . . . . . . . . . . . . 14 (norm‘𝑇) = (norm‘𝑇)
10 eqid 2758 . . . . . . . . . . . . . 14 (0g𝑇) = (0g𝑇)
118, 9, 10nmeq0 23325 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)))
12 eqid 2758 . . . . . . . . . . . . . 14 (invg𝑇) = (invg𝑇)
138, 9, 12nminv 23328 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))
14 eqid 2758 . . . . . . . . . . . . . . . 16 (+g𝑇) = (+g𝑇)
158, 9, 14nmtri 23333 . . . . . . . . . . . . . . 15 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
16153expa 1115 . . . . . . . . . . . . . 14 (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1716ralrimiva 3113 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1811, 13, 173jca 1125 . . . . . . . . . . . 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 485 . . . . . . . . . 10 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
21203ad2ant1 1130 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
225, 1tngbas 23348 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝑋 = (Base‘𝑇))
23 tngngp3.p . . . . . . . . . . . . . . 15 + = (+g𝐺)
245, 23tngplusg 23349 . . . . . . . . . . . . . 14 (𝑁 ∈ V → + = (+g𝑇))
25 tngngp3.i . . . . . . . . . . . . . . 15 𝐼 = (invg𝐺)
26 eqidd 2759 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝐺))
27 eqid 2758 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) = (Base‘𝐺)
285, 27tngbas 23348 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝑇))
29 eqid 2758 . . . . . . . . . . . . . . . . . . 19 (+g𝐺) = (+g𝐺)
305, 29tngplusg 23349 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ V → (+g𝐺) = (+g𝑇))
3130oveqd 7172 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ V → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3231adantr 484 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3326, 28, 32grpinvpropd 18246 . . . . . . . . . . . . . . 15 (𝑁 ∈ V → (invg𝐺) = (invg𝑇))
3425, 33syl5eq 2805 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝐼 = (invg𝑇))
3522, 24, 343jca 1125 . . . . . . . . . . . . 13 (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
3635adantr 484 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
37363ad2ant1 1130 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
38 reex 10671 . . . . . . . . . . . . 13 ℝ ∈ V
395, 1, 38tngnm 23358 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
40393adant1 1127 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
41 tngngp3.z . . . . . . . . . . . . . 14 0 = (0g𝐺)
425, 41tng0 23350 . . . . . . . . . . . . 13 (𝑁 ∈ V → 0 = (0g𝑇))
4342adantr 484 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 = (0g𝑇))
44433ad2ant1 1130 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 = (0g𝑇))
4537, 40, 443jca 1125 . . . . . . . . . 10 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)))
46 simp1 1133 . . . . . . . . . . . 12 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝑋 = (Base‘𝑇))
47463ad2ant1 1130 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑋 = (Base‘𝑇))
48 simp2 1134 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑁 = (norm‘𝑇))
4948fveq1d 6664 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
5049eqeq1d 2760 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0))
51 simp3 1135 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 0 = (0g𝑇))
5251eqeq2d 2769 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 = 0𝑥 = (0g𝑇)))
5350, 52bibi12d 349 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇))))
54 simp3 1135 . . . . . . . . . . . . . . . 16 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝐼 = (invg𝑇))
55543ad2ant1 1130 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝐼 = (invg𝑇))
5655fveq1d 6664 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝐼𝑥) = ((invg𝑇)‘𝑥))
5748, 56fveq12d 6669 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝐼𝑥)) = ((norm‘𝑇)‘((invg𝑇)‘𝑥)))
5857, 49eqeq12d 2774 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)))
59 simp2 1134 . . . . . . . . . . . . . . . . 17 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → + = (+g𝑇))
60593ad2ant1 1130 . . . . . . . . . . . . . . . 16 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → + = (+g𝑇))
6160oveqd 7172 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 + 𝑦) = (𝑥(+g𝑇)𝑦))
6248, 61fveq12d 6669 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)))
63 fveq1 6661 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
64 fveq1 6661 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑦) = ((norm‘𝑇)‘𝑦))
6563, 64oveq12d 7173 . . . . . . . . . . . . . . 15 (𝑁 = (norm‘𝑇) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
66653ad2ant2 1131 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
6762, 66breq12d 5048 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6847, 67raleqbidv 3319 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6953, 58, 683anbi123d 1433 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7047, 69raleqbidv 3319 . . . . . . . . . 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 260 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
737, 72jca 515 . . . . . . 7 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
74733exp 1116 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
756, 74mpd 15 . . . . 5 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
7675expcom 417 . . . 4 (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
7776com13 88 . . 3 (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
784, 77mpd 15 . 2 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
79 eqid 2758 . . . 4 (-g𝐺) = (-g𝐺)
80 simpl 486 . . . . 5 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝐺 ∈ Grp)
8180adantl 485 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝐺 ∈ Grp)
82 simpl 486 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑁:𝑋⟶ℝ)
83 fveq2 6662 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁𝑥) = (𝑁𝑎))
8483eqeq1d 2760 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁𝑥) = 0 ↔ (𝑁𝑎) = 0))
85 eqeq1 2762 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥 = 0𝑎 = 0 ))
8684, 85bibi12d 349 . . . . . . . . . . 11 (𝑥 = 𝑎 → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
87 fveq2 6662 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝐼𝑥) = (𝐼𝑎))
8887fveq2d 6666 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑎)))
8988, 83eqeq12d 2774 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑎)) = (𝑁𝑎)))
90 fvoveq1 7178 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦)))
9183oveq1d 7170 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝑁𝑥) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁𝑦)))
9290, 91breq12d 5048 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9392ralbidv 3126 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9486, 89, 933anbi123d 1433 . . . . . . . . . 10 (𝑥 = 𝑎 → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)))))
9594rspccva 3542 . . . . . . . . 9 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
96 simp1 1133 . . . . . . . . 9 ((((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9795, 96syl 17 . . . . . . . 8 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9897ex 416 . . . . . . 7 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
9998adantl 485 . . . . . 6 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
10099adantl 485 . . . . 5 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
101100imp 410 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
1021, 23, 25, 79grpsubval 18221 . . . . . . 7 ((𝑎𝑋𝑏𝑋) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
103102adantl 485 . . . . . 6 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
104103fveq2d 6666 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼𝑏))))
105 3simpc 1147 . . . . . . . . . 10 ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
106105ralimi 3092 . . . . . . . . 9 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
107 simpr 488 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
108107ralimi 3092 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
109 oveq2 7163 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼𝑏)))
110109fveq2d 6666 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼𝑏))))
111 fveq2 6662 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑁𝑦) = (𝑁‘(𝐼𝑏)))
112111oveq2d 7171 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → ((𝑁𝑎) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
113110, 112breq12d 5048 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐼𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
11492, 113rspc2v 3553 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋) → (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
1151, 25grpinvcl 18223 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝑏𝑋) → (𝐼𝑏) ∈ 𝑋)
116115ex 416 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ Grp → (𝑏𝑋 → (𝐼𝑏) ∈ 𝑋))
117116anim2d 614 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋)))
118117imp 410 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋))
119114, 118syl11 33 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
120119expd 419 . . . . . . . . . . . . . . 15 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
121108, 120syl 17 . . . . . . . . . . . . . 14 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
122121imp 410 . . . . . . . . . . . . 13 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
123122imp 410 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
124 simpl 486 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
125124ralimi 3092 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
126 fveq2 6662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐼𝑥) = (𝐼𝑏))
127126fveq2d 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑏)))
128 fveq2 6662 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁𝑥) = (𝑁𝑏))
129127, 128eqeq12d 2774 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑏)) = (𝑁𝑏)))
130129rspccva 3542 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁‘(𝐼𝑏)) = (𝑁𝑏))
131130eqcomd 2764 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
132131ex 416 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
133125, 132syl 17 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
134133adantr 484 . . . . . . . . . . . . . . 15 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
135134adantld 494 . . . . . . . . . . . . . 14 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
136135imp 410 . . . . . . . . . . . . 13 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
137136oveq2d 7171 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑁𝑎) + (𝑁𝑏)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
138123, 137breqtrrd 5063 . . . . . . . . . . 11 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
139138ex 416 . . . . . . . . . 10 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
140139ex 416 . . . . . . . . 9 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
141106, 140syl 17 . . . . . . . 8 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
142141impcom 411 . . . . . . 7 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
143142adantl 485 . . . . . 6 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
144143imp 410 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
145104, 144eqbrtrd 5057 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) ≤ ((𝑁𝑎) + (𝑁𝑏)))
1465, 1, 79, 41, 81, 82, 101, 145tngngpd 23360 . . 3 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑇 ∈ NrmGrp)
147146ex 416 . 2 (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝑇 ∈ NrmGrp))
14878, 147impbid 215 1 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  Vcvv 3409   class class class wbr 5035  ⟶wf 6335  ‘cfv 6339  (class class class)co 7155  ℝcr 10579  0cc0 10580   + caddc 10583   ≤ cle 10719  Basecbs 16546  +gcplusg 16628  0gc0g 16776  Grpcgrp 18174  invgcminusg 18175  -gcsg 18176  normcnm 23283  NrmGrpcngp 23284   toNrmGrp ctng 23285 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657  ax-pre-sup 10658 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-1st 7698  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-er 8304  df-map 8423  df-en 8533  df-dom 8534  df-sdom 8535  df-sup 8944  df-inf 8945  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749  df-n0 11940  df-z 12026  df-dec 12143  df-uz 12288  df-q 12394  df-rp 12436  df-xneg 12553  df-xadd 12554  df-xmul 12555  df-ndx 16549  df-slot 16550  df-base 16552  df-sets 16553  df-plusg 16641  df-tset 16647  df-ds 16650  df-rest 16759  df-topn 16760  df-0g 16778  df-topgen 16780  df-mgm 17923  df-sgrp 17972  df-mnd 17983  df-grp 18177  df-minusg 18178  df-sbg 18179  df-psmet 20163  df-xmet 20164  df-met 20165  df-bl 20166  df-mopn 20167  df-top 21599  df-topon 21616  df-topsp 21638  df-bases 21651  df-xms 23027  df-ms 23028  df-nm 23289  df-ngp 23290  df-tng 23291 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator