Step | Hyp | Ref
| Expression |
1 | | tngngp.t |
. . . . 5
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) |
2 | | tngngp.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
3 | | eqid 2622 |
. . . . 5
⊢
(dist‘𝑇) =
(dist‘𝑇) |
4 | 1, 2, 3 | tngngp2 22456 |
. . . 4
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ (dist‘𝑇) ∈ (Met‘𝑋)))) |
5 | 4 | simprbda 653 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp) |
6 | | simplr 792 |
. . . . . . 7
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑇 ∈ NrmGrp) |
7 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
8 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺)
∈ V |
9 | 2, 8 | eqeltri 2697 |
. . . . . . . . . . 11
⊢ 𝑋 ∈ V |
10 | | reex 10027 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
11 | | fex2 7121 |
. . . . . . . . . . 11
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V) →
𝑁 ∈
V) |
12 | 9, 10, 11 | mp3an23 1416 |
. . . . . . . . . 10
⊢ (𝑁:𝑋⟶ℝ → 𝑁 ∈ V) |
13 | 12 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑁 ∈ V) |
14 | 1, 2 | tngbas 22445 |
. . . . . . . . 9
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝑇)) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑋 = (Base‘𝑇)) |
16 | 7, 15 | eleqtrd 2703 |
. . . . . . 7
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (Base‘𝑇)) |
17 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑇) =
(Base‘𝑇) |
18 | | eqid 2622 |
. . . . . . . 8
⊢
(norm‘𝑇) =
(norm‘𝑇) |
19 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑇) = (0g‘𝑇) |
20 | 17, 18, 19 | nmeq0 22422 |
. . . . . . 7
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇))) |
21 | 6, 16, 20 | syl2anc 693 |
. . . . . 6
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇))) |
22 | 5 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) |
23 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑁:𝑋⟶ℝ) |
24 | 1, 2, 10 | tngnm 22455 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇)) |
25 | 22, 23, 24 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 𝑁 = (norm‘𝑇)) |
26 | 25 | fveq1d 6193 |
. . . . . . 7
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑁‘𝑥) = ((norm‘𝑇)‘𝑥)) |
27 | 26 | eqeq1d 2624 |
. . . . . 6
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0)) |
28 | | tngngp.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
29 | 1, 28 | tng0 22447 |
. . . . . . . 8
⊢ (𝑁 ∈ V → 0 =
(0g‘𝑇)) |
30 | 13, 29 | syl 17 |
. . . . . . 7
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → 0 =
(0g‘𝑇)) |
31 | 30 | eqeq2d 2632 |
. . . . . 6
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑥 = 0 ↔ 𝑥 = (0g‘𝑇))) |
32 | 21, 27, 31 | 3bitr4d 300 |
. . . . 5
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 )) |
33 | | simpllr 799 |
. . . . . . . 8
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑇 ∈ NrmGrp) |
34 | 16 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ (Base‘𝑇)) |
35 | 15 | eleq2d 2687 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ (Base‘𝑇))) |
36 | 35 | biimpa 501 |
. . . . . . . 8
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ (Base‘𝑇)) |
37 | | eqid 2622 |
. . . . . . . . 9
⊢
(-g‘𝑇) = (-g‘𝑇) |
38 | 17, 18, 37 | nmmtri 22426 |
. . . . . . . 8
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(-g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
39 | 33, 34, 36, 38 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((norm‘𝑇)‘(𝑥(-g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
40 | | tngngp.m |
. . . . . . . . . . 11
⊢ − =
(-g‘𝐺) |
41 | 2, 15 | syl5eqr 2670 |
. . . . . . . . . . . 12
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (Base‘𝐺) = (Base‘𝑇)) |
42 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐺) = (+g‘𝐺) |
43 | 1, 42 | tngplusg 22446 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ V →
(+g‘𝐺) =
(+g‘𝑇)) |
44 | 13, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (+g‘𝐺) = (+g‘𝑇)) |
45 | 41, 44 | grpsubpropd 17520 |
. . . . . . . . . . 11
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (-g‘𝐺) = (-g‘𝑇)) |
46 | 40, 45 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → − =
(-g‘𝑇)) |
47 | 46 | oveqd 6667 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝑦) = (𝑥(-g‘𝑇)𝑦)) |
48 | 25, 47 | fveq12d 6197 |
. . . . . . . 8
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑥 − 𝑦)) = ((norm‘𝑇)‘(𝑥(-g‘𝑇)𝑦))) |
49 | 48 | adantr 481 |
. . . . . . 7
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥 − 𝑦)) = ((norm‘𝑇)‘(𝑥(-g‘𝑇)𝑦))) |
50 | 25 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (𝑁‘𝑦) = ((norm‘𝑇)‘𝑦)) |
51 | 26, 50 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) + (𝑁‘𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
52 | 51 | adantr 481 |
. . . . . . 7
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑥) + (𝑁‘𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
53 | 39, 49, 52 | 3brtr4d 4685 |
. . . . . 6
⊢ ((((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
54 | 53 | ralrimiva 2966 |
. . . . 5
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
55 | 32, 54 | jca 554 |
. . . 4
⊢ (((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) ∧ 𝑥 ∈ 𝑋) → (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) |
56 | 55 | ralrimiva 2966 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) |
57 | 5, 56 | jca 554 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) |
58 | | simprl 794 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝐺 ∈ Grp) |
59 | | simpl 473 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝑁:𝑋⟶ℝ) |
60 | | simpl 473 |
. . . . . 6
⊢ ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 )) |
61 | 60 | ralimi 2952 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 )) |
62 | 61 | ad2antll 765 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 )) |
63 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝑁‘𝑥) = (𝑁‘𝑎)) |
64 | 63 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝑁‘𝑥) = 0 ↔ (𝑁‘𝑎) = 0)) |
65 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑥 = 𝑎 → (𝑥 = 0 ↔ 𝑎 = 0 )) |
66 | 64, 65 | bibi12d 335 |
. . . . 5
⊢ (𝑥 = 𝑎 → (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ))) |
67 | 66 | rspccva 3308 |
. . . 4
⊢
((∀𝑥 ∈
𝑋 ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ 𝑎 ∈ 𝑋) → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 )) |
68 | 62, 67 | sylan 488 |
. . 3
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ 𝑎 ∈ 𝑋) → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 )) |
69 | | simpr 477 |
. . . . . 6
⊢ ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
70 | 69 | ralimi 2952 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
71 | 70 | ad2antll 765 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
72 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑥 − 𝑦) = (𝑎 − 𝑦)) |
73 | 72 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝑁‘(𝑥 − 𝑦)) = (𝑁‘(𝑎 − 𝑦))) |
74 | 63 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → ((𝑁‘𝑥) + (𝑁‘𝑦)) = ((𝑁‘𝑎) + (𝑁‘𝑦))) |
75 | 73, 74 | breq12d 4666 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ (𝑁‘(𝑎 − 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)))) |
76 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (𝑎 − 𝑦) = (𝑎 − 𝑏)) |
77 | 76 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝑁‘(𝑎 − 𝑦)) = (𝑁‘(𝑎 − 𝑏))) |
78 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (𝑁‘𝑦) = (𝑁‘𝑏)) |
79 | 78 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → ((𝑁‘𝑎) + (𝑁‘𝑦)) = ((𝑁‘𝑎) + (𝑁‘𝑏))) |
80 | 77, 79 | breq12d 4666 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝑁‘(𝑎 − 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)) ↔ (𝑁‘(𝑎 − 𝑏)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏)))) |
81 | 75, 80 | rspc2va 3323 |
. . . . 5
⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝑁‘(𝑎 − 𝑏)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
82 | 81 | ancoms 469 |
. . . 4
⊢
((∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 − 𝑏)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
83 | 71, 82 | sylan 488 |
. . 3
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 − 𝑏)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
84 | 1, 2, 40, 28, 58, 59, 68, 83 | tngngpd 22457 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝑇 ∈ NrmGrp) |
85 | 57, 84 | impbida 877 |
1
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) |