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

Theorem tngngp3 23182
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 6680 . . . 4 𝑋 ∈ V
3 fex 6987 . . . 4 ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V)
42, 3mpan2 687 . . 3 (𝑁:𝑋⟶ℝ → 𝑁 ∈ V)
5 tngngp3.t . . . . . . 7 𝑇 = (𝐺 toNrmGrp 𝑁)
65tnggrpr 23181 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp)
7 simp2 1131 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp)
8 eqid 2825 . . . . . . . . . . . . . 14 (Base‘𝑇) = (Base‘𝑇)
9 eqid 2825 . . . . . . . . . . . . . 14 (norm‘𝑇) = (norm‘𝑇)
10 eqid 2825 . . . . . . . . . . . . . 14 (0g𝑇) = (0g𝑇)
118, 9, 10nmeq0 23144 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)))
12 eqid 2825 . . . . . . . . . . . . . 14 (invg𝑇) = (invg𝑇)
138, 9, 12nminv 23147 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))
14 eqid 2825 . . . . . . . . . . . . . . . 16 (+g𝑇) = (+g𝑇)
158, 9, 14nmtri 23152 . . . . . . . . . . . . . . 15 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
16153expa 1112 . . . . . . . . . . . . . 14 (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1716ralrimiva 3186 . . . . . . . . . . . . 13 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
1811, 13, 173jca 1122 . . . . . . . . . . . 12 ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
1918ralrimiva 3186 . . . . . . . . . . 11 (𝑇 ∈ NrmGrp → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
2019adantl 482 . . . . . . . . . 10 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
21203ad2ant1 1127 . . . . . . . . 9 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
225, 1tngbas 23167 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝑋 = (Base‘𝑇))
23 tngngp3.p . . . . . . . . . . . . . . 15 + = (+g𝐺)
245, 23tngplusg 23168 . . . . . . . . . . . . . 14 (𝑁 ∈ V → + = (+g𝑇))
25 tngngp3.i . . . . . . . . . . . . . . 15 𝐼 = (invg𝐺)
26 eqidd 2826 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝐺))
27 eqid 2825 . . . . . . . . . . . . . . . . 17 (Base‘𝐺) = (Base‘𝐺)
285, 27tngbas 23167 . . . . . . . . . . . . . . . 16 (𝑁 ∈ V → (Base‘𝐺) = (Base‘𝑇))
29 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (+g𝐺) = (+g𝐺)
305, 29tngplusg 23168 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ V → (+g𝐺) = (+g𝑇))
3130oveqd 7168 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ V → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3231adantr 481 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝑇)𝑦))
3326, 28, 32grpinvpropd 18106 . . . . . . . . . . . . . . 15 (𝑁 ∈ V → (invg𝐺) = (invg𝑇))
3425, 33syl5eq 2872 . . . . . . . . . . . . . 14 (𝑁 ∈ V → 𝐼 = (invg𝑇))
3522, 24, 343jca 1122 . . . . . . . . . . . . 13 (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
3635adantr 481 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
37363ad2ant1 1127 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)))
38 reex 10620 . . . . . . . . . . . . 13 ℝ ∈ V
395, 1, 38tngnm 23177 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
40393adant1 1124 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇))
41 tngngp3.z . . . . . . . . . . . . . 14 0 = (0g𝐺)
425, 41tng0 23169 . . . . . . . . . . . . 13 (𝑁 ∈ V → 0 = (0g𝑇))
4342adantr 481 . . . . . . . . . . . 12 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 = (0g𝑇))
44433ad2ant1 1127 . . . . . . . . . . 11 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 = (0g𝑇))
4537, 40, 443jca 1122 . . . . . . . . . 10 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)))
46 simp1 1130 . . . . . . . . . . . 12 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝑋 = (Base‘𝑇))
47463ad2ant1 1127 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑋 = (Base‘𝑇))
48 simp2 1131 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝑁 = (norm‘𝑇))
4948fveq1d 6668 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
5049eqeq1d 2827 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0))
51 simp3 1132 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 0 = (0g𝑇))
5251eqeq2d 2836 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 = 0𝑥 = (0g𝑇)))
5350, 52bibi12d 347 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇))))
54 simp3 1132 . . . . . . . . . . . . . . . 16 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → 𝐼 = (invg𝑇))
55543ad2ant1 1127 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → 𝐼 = (invg𝑇))
5655fveq1d 6668 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝐼𝑥) = ((invg𝑇)‘𝑥))
5748, 56fveq12d 6673 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝐼𝑥)) = ((norm‘𝑇)‘((invg𝑇)‘𝑥)))
5857, 49eqeq12d 2841 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)))
59 simp2 1131 . . . . . . . . . . . . . . . . 17 ((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) → + = (+g𝑇))
60593ad2ant1 1127 . . . . . . . . . . . . . . . 16 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → + = (+g𝑇))
6160oveqd 7168 . . . . . . . . . . . . . . 15 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑥 + 𝑦) = (𝑥(+g𝑇)𝑦))
6248, 61fveq12d 6673 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)))
63 fveq1 6665 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑥) = ((norm‘𝑇)‘𝑥))
64 fveq1 6665 . . . . . . . . . . . . . . . 16 (𝑁 = (norm‘𝑇) → (𝑁𝑦) = ((norm‘𝑇)‘𝑦))
6563, 64oveq12d 7169 . . . . . . . . . . . . . . 15 (𝑁 = (norm‘𝑇) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
66653ad2ant2 1128 . . . . . . . . . . . . . 14 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁𝑥) + (𝑁𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))
6762, 66breq12d 5075 . . . . . . . . . . . . 13 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6847, 67raleqbidv 3406 . . . . . . . . . . . 12 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))
6953, 58, 683anbi123d 1429 . . . . . . . . . . 11 (((𝑋 = (Base‘𝑇) ∧ + = (+g𝑇) ∧ 𝐼 = (invg𝑇)) ∧ 𝑁 = (norm‘𝑇) ∧ 0 = (0g𝑇)) → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g𝑇)) ∧ ((norm‘𝑇)‘((invg𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))))
7047, 69raleqbidv 3406 . . . . . . . . . 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 258 . . . . . . . 8 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
737, 72jca 512 . . . . . . 7 (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
74733exp 1113 . . . . . 6 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
756, 74mpd 15 . . . . 5 ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
7675expcom 414 . . . 4 (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
7776com13 88 . . 3 (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))))
784, 77mpd 15 . 2 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
79 eqid 2825 . . . 4 (-g𝐺) = (-g𝐺)
80 simpl 483 . . . . 5 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝐺 ∈ Grp)
8180adantl 482 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝐺 ∈ Grp)
82 simpl 483 . . . 4 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑁:𝑋⟶ℝ)
83 fveq2 6666 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁𝑥) = (𝑁𝑎))
8483eqeq1d 2827 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁𝑥) = 0 ↔ (𝑁𝑎) = 0))
85 eqeq1 2829 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑥 = 0𝑎 = 0 ))
8684, 85bibi12d 347 . . . . . . . . . . 11 (𝑥 = 𝑎 → (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
87 fveq2 6666 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝐼𝑥) = (𝐼𝑎))
8887fveq2d 6670 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑎)))
8988, 83eqeq12d 2841 . . . . . . . . . . 11 (𝑥 = 𝑎 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑎)) = (𝑁𝑎)))
90 fvoveq1 7174 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦)))
9183oveq1d 7166 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝑁𝑥) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁𝑦)))
9290, 91breq12d 5075 . . . . . . . . . . . 12 (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9392ralbidv 3201 . . . . . . . . . . 11 (𝑥 = 𝑎 → (∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
9486, 89, 933anbi123d 1429 . . . . . . . . . 10 (𝑥 = 𝑎 → ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ↔ (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)))))
9594rspccva 3625 . . . . . . . . 9 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → (((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))))
96 simp1 1130 . . . . . . . . 9 ((((𝑁𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼𝑎)) = (𝑁𝑎) ∧ ∀𝑦𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦))) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9795, 96syl 17 . . . . . . . 8 ((∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
9897ex 413 . . . . . . 7 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
9998adantl 482 . . . . . 6 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
10099adantl 482 . . . . 5 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → (𝑎𝑋 → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 )))
101100imp 407 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ 𝑎𝑋) → ((𝑁𝑎) = 0 ↔ 𝑎 = 0 ))
1021, 23, 25, 79grpsubval 18081 . . . . . . 7 ((𝑎𝑋𝑏𝑋) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
103102adantl 482 . . . . . 6 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(-g𝐺)𝑏) = (𝑎 + (𝐼𝑏)))
104103fveq2d 6670 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼𝑏))))
105 3simpc 1144 . . . . . . . . . 10 ((((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
106105ralimi 3164 . . . . . . . . 9 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
107 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
108107ralimi 3164 . . . . . . . . . . . . . . 15 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))
109 oveq2 7159 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼𝑏)))
110109fveq2d 6670 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼𝑏))))
111 fveq2 6666 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐼𝑏) → (𝑁𝑦) = (𝑁‘(𝐼𝑏)))
112111oveq2d 7167 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐼𝑏) → ((𝑁𝑎) + (𝑁𝑦)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
113110, 112breq12d 5075 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐼𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁𝑎) + (𝑁𝑦)) ↔ (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
11492, 113rspc2v 3636 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋) → (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
1151, 25grpinvcl 18083 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝑏𝑋) → (𝐼𝑏) ∈ 𝑋)
116115ex 413 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ Grp → (𝑏𝑋 → (𝐼𝑏) ∈ 𝑋))
117116anim2d 611 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋)))
118117imp 407 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝑋 ∧ (𝐼𝑏) ∈ 𝑋))
119114, 118syl11 33 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
120119expd 416 . . . . . . . . . . . . . . 15 (∀𝑥𝑋𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
121108, 120syl 17 . . . . . . . . . . . . . 14 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))))
122121imp 407 . . . . . . . . . . . . 13 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏)))))
123122imp 407 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
124 simpl 483 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
125124ralimi 3164 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → ∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥))
126 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → (𝐼𝑥) = (𝐼𝑏))
127126fveq2d 6670 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁‘(𝐼𝑥)) = (𝑁‘(𝐼𝑏)))
128 fveq2 6666 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑏 → (𝑁𝑥) = (𝑁𝑏))
129127, 128eqeq12d 2841 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑏 → ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ↔ (𝑁‘(𝐼𝑏)) = (𝑁𝑏)))
130129rspccva 3625 . . . . . . . . . . . . . . . . . . 19 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁‘(𝐼𝑏)) = (𝑁𝑏))
131130eqcomd 2831 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ 𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
132131ex 413 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑋 (𝑁‘(𝐼𝑥)) = (𝑁𝑥) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
133125, 132syl 17 . . . . . . . . . . . . . . . 16 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
134133adantr 481 . . . . . . . . . . . . . . 15 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏𝑋 → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
135134adantld 491 . . . . . . . . . . . . . 14 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁𝑏) = (𝑁‘(𝐼𝑏))))
136135imp 407 . . . . . . . . . . . . 13 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁𝑏) = (𝑁‘(𝐼𝑏)))
137136oveq2d 7167 . . . . . . . . . . . 12 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑁𝑎) + (𝑁𝑏)) = ((𝑁𝑎) + (𝑁‘(𝐼𝑏))))
138123, 137breqtrrd 5090 . . . . . . . . . . 11 (((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
139138ex 413 . . . . . . . . . 10 ((∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
140139ex 413 . . . . . . . . 9 (∀𝑥𝑋 ((𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
141106, 140syl 17 . . . . . . . 8 (∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))) → (𝐺 ∈ Grp → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))))
142141impcom 408 . . . . . . 7 ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
143142adantl 482 . . . . . 6 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → ((𝑎𝑋𝑏𝑋) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏))))
144143imp 407 . . . . 5 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎 + (𝐼𝑏))) ≤ ((𝑁𝑎) + (𝑁𝑏)))
145104, 144eqbrtrd 5084 . . . 4 (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) ∧ (𝑎𝑋𝑏𝑋)) → (𝑁‘(𝑎(-g𝐺)𝑏)) ≤ ((𝑁𝑎) + (𝑁𝑏)))
1465, 1, 79, 41, 81, 82, 101, 145tngngpd 23179 . . 3 ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))) → 𝑇 ∈ NrmGrp)
147146ex 413 . 2 (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))) → 𝑇 ∈ NrmGrp))
14878, 147impbid 213 1 (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼𝑥)) = (𝑁𝑥) ∧ ∀𝑦𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wral 3142  Vcvv 3499   class class class wbr 5062  wf 6347  cfv 6351  (class class class)co 7151  cr 10528  0cc0 10529   + caddc 10532  cle 10668  Basecbs 16475  +gcplusg 16557  0gc0g 16705  Grpcgrp 18035  invgcminusg 18036  -gcsg 18037  normcnm 23103  NrmGrpcngp 23104   toNrmGrp ctng 23105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-plusg 16570  df-tset 16576  df-ds 16579  df-rest 16688  df-topn 16689  df-0g 16707  df-topgen 16709  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-grp 18038  df-minusg 18039  df-sbg 18040  df-psmet 20455  df-xmet 20456  df-met 20457  df-bl 20458  df-mopn 20459  df-top 21420  df-topon 21437  df-topsp 21459  df-bases 21472  df-xms 22847  df-ms 22848  df-nm 23109  df-ngp 23110  df-tng 23111
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator