Step | Hyp | Ref
| Expression |
1 | | tngngp3.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
2 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝐺)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . 4
⊢ 𝑋 ∈ V |
4 | | fex 6490 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V) → 𝑁 ∈ V) |
5 | 3, 4 | mpan2 707 |
. . 3
⊢ (𝑁:𝑋⟶ℝ → 𝑁 ∈ V) |
6 | | tngngp3.t |
. . . . . . 7
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) |
7 | 6 | tnggrpr 22459 |
. . . . . 6
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp) |
8 | | simp2 1062 |
. . . . . . . 8
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝐺 ∈ Grp) |
9 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑇) =
(Base‘𝑇) |
10 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(norm‘𝑇) =
(norm‘𝑇) |
11 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑇) = (0g‘𝑇) |
12 | 9, 10, 11 | nmeq0 22422 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → (((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇))) |
13 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(invg‘𝑇) = (invg‘𝑇) |
14 | 9, 10, 13 | nminv 22425 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥)) |
15 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘𝑇) = (+g‘𝑇) |
16 | 9, 10, 15 | nmtri 22430 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
17 | 16 | 3expa 1265 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) ∧ 𝑦 ∈ (Base‘𝑇)) → ((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
18 | 17 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
19 | 12, 14, 18 | 3jca 1242 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝑇)) → ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
20 | 19 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ NrmGrp →
∀𝑥 ∈
(Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
21 | 20 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) →
∀𝑥 ∈
(Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
22 | 21 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
23 | 6, 1 | tngbas 22445 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝑇)) |
24 | | tngngp3.p |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘𝐺) |
25 | 6, 24 | tngplusg 22446 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → + =
(+g‘𝑇)) |
26 | | tngngp3.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (invg‘𝐺) |
27 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ V →
(Base‘𝐺) =
(Base‘𝐺)) |
28 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐺) =
(Base‘𝐺) |
29 | 6, 28 | tngbas 22445 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ V →
(Base‘𝐺) =
(Base‘𝑇)) |
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(+g‘𝐺) = (+g‘𝐺) |
31 | 6, 30 | tngplusg 22446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ V →
(+g‘𝐺) =
(+g‘𝑇)) |
32 | 31 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ V → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝑇)𝑦)) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ V ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝑇)𝑦)) |
34 | 27, 29, 33 | grpinvpropd 17490 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ V →
(invg‘𝐺) =
(invg‘𝑇)) |
35 | 26, 34 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ V → 𝐼 = (invg‘𝑇)) |
36 | 23, 25, 35 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ V → (𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))) |
37 | 36 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))) |
38 | 37 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))) |
39 | | reex 10027 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
40 | 6, 1, 39 | tngnm 22455 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇)) |
41 | 40 | 3adant1 1079 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇)) |
42 | | tngngp3.z |
. . . . . . . . . . . . . 14
⊢ 0 =
(0g‘𝐺) |
43 | 6, 42 | tng0 22447 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ V → 0 =
(0g‘𝑇)) |
44 | 43 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → 0 =
(0g‘𝑇)) |
45 | 44 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 0 =
(0g‘𝑇)) |
46 | 38, 41, 45 | 3jca 1242 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))) |
47 | | simp1 1061 |
. . . . . . . . . . . 12
⊢ ((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
→ 𝑋 =
(Base‘𝑇)) |
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ 𝑋 =
(Base‘𝑇)) |
49 | | simp2 1062 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ 𝑁 =
(norm‘𝑇)) |
50 | 49 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝑁‘𝑥) = ((norm‘𝑇)‘𝑥)) |
51 | 50 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ ((𝑁‘𝑥) = 0 ↔ ((norm‘𝑇)‘𝑥) = 0)) |
52 | | simp3 1063 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ 0
= (0g‘𝑇)) |
53 | 52 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝑥 = 0 ↔ 𝑥 = (0g‘𝑇))) |
54 | 51, 53 | bibi12d 335 |
. . . . . . . . . . . 12
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔
(((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)))) |
55 | | simp3 1063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
→ 𝐼 =
(invg‘𝑇)) |
56 | 55 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ 𝐼 =
(invg‘𝑇)) |
57 | 56 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝐼‘𝑥) =
((invg‘𝑇)‘𝑥)) |
58 | 49, 57 | fveq12d 6197 |
. . . . . . . . . . . . 13
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝑁‘(𝐼‘𝑥)) = ((norm‘𝑇)‘((invg‘𝑇)‘𝑥))) |
59 | 58, 50 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ↔ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥))) |
60 | | simp2 1062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
→ +
= (+g‘𝑇)) |
61 | 60 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ +
= (+g‘𝑇)) |
62 | 61 | oveqd 6667 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝑥 + 𝑦) = (𝑥(+g‘𝑇)𝑦)) |
63 | 49, 62 | fveq12d 6197 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (𝑁‘(𝑥 + 𝑦)) = ((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦))) |
64 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (norm‘𝑇) → (𝑁‘𝑥) = ((norm‘𝑇)‘𝑥)) |
65 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (norm‘𝑇) → (𝑁‘𝑦) = ((norm‘𝑇)‘𝑦)) |
66 | 64, 65 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (norm‘𝑇) → ((𝑁‘𝑥) + (𝑁‘𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
67 | 66 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ ((𝑁‘𝑥) + (𝑁‘𝑦)) = (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))) |
68 | 63, 67 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ ((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
69 | 48, 68 | raleqbidv 3152 |
. . . . . . . . . . . 12
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (∀𝑦 ∈
𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦)))) |
70 | 54, 59, 69 | 3anbi123d 1399 |
. . . . . . . . . . 11
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ ((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))) |
71 | 48, 70 | raleqbidv 3152 |
. . . . . . . . . 10
⊢ (((𝑋 = (Base‘𝑇) ∧ + =
(+g‘𝑇)
∧ 𝐼 =
(invg‘𝑇))
∧ 𝑁 = (norm‘𝑇) ∧ 0 =
(0g‘𝑇))
→ (∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))) |
72 | 46, 71 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑇)((((norm‘𝑇)‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑇)) ∧ ((norm‘𝑇)‘((invg‘𝑇)‘𝑥)) = ((norm‘𝑇)‘𝑥) ∧ ∀𝑦 ∈ (Base‘𝑇)((norm‘𝑇)‘(𝑥(+g‘𝑇)𝑦)) ≤ (((norm‘𝑇)‘𝑥) + ((norm‘𝑇)‘𝑦))))) |
73 | 22, 72 | mpbird 247 |
. . . . . . . 8
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) |
74 | 8, 73 | jca 554 |
. . . . . . 7
⊢ (((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) ∧ 𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) |
75 | 74 | 3exp 1264 |
. . . . . 6
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))) |
76 | 7, 75 | mpd 15 |
. . . . 5
⊢ ((𝑁 ∈ V ∧ 𝑇 ∈ NrmGrp) → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) |
77 | 76 | expcom 451 |
. . . 4
⊢ (𝑇 ∈ NrmGrp → (𝑁 ∈ V → (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))) |
78 | 77 | com13 88 |
. . 3
⊢ (𝑁:𝑋⟶ℝ → (𝑁 ∈ V → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))) |
79 | 5, 78 | mpd 15 |
. 2
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) |
80 | | eqid 2622 |
. . . 4
⊢
(-g‘𝐺) = (-g‘𝐺) |
81 | | simpl 473 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) → 𝐺 ∈ Grp) |
82 | 81 | adantl 482 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝐺 ∈ Grp) |
83 | | simpl 473 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝑁:𝑋⟶ℝ) |
84 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑁‘𝑥) = (𝑁‘𝑎)) |
85 | 84 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((𝑁‘𝑥) = 0 ↔ (𝑁‘𝑎) = 0)) |
86 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑥 = 0 ↔ 𝑎 = 0 )) |
87 | 85, 86 | bibi12d 335 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ↔ ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ))) |
88 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝐼‘𝑥) = (𝐼‘𝑎)) |
89 | 88 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (𝑁‘(𝐼‘𝑥)) = (𝑁‘(𝐼‘𝑎))) |
90 | 89, 84 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ↔ (𝑁‘(𝐼‘𝑎)) = (𝑁‘𝑎))) |
91 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦)) |
92 | 91 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑁‘(𝑥 + 𝑦)) = (𝑁‘(𝑎 + 𝑦))) |
93 | 84 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → ((𝑁‘𝑥) + (𝑁‘𝑦)) = ((𝑁‘𝑎) + (𝑁‘𝑦))) |
94 | 92, 93 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)))) |
95 | 94 | ralbidv 2986 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)))) |
96 | 87, 90, 95 | 3anbi123d 1399 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ↔ (((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼‘𝑎)) = (𝑁‘𝑎) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦))))) |
97 | 96 | rspccva 3308 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝑎 ∈ 𝑋) → (((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼‘𝑎)) = (𝑁‘𝑎) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)))) |
98 | | simp1 1061 |
. . . . . . . . 9
⊢ ((((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ) ∧ (𝑁‘(𝐼‘𝑎)) = (𝑁‘𝑎) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦))) → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 )) |
99 | 97, 98 | syl 17 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝑎 ∈ 𝑋) → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 )) |
100 | 99 | ex 450 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝑎 ∈ 𝑋 → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ))) |
101 | 100 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) → (𝑎 ∈ 𝑋 → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ))) |
102 | 101 | adantl 482 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → (𝑎 ∈ 𝑋 → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 ))) |
103 | 102 | imp 445 |
. . . 4
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ 𝑎 ∈ 𝑋) → ((𝑁‘𝑎) = 0 ↔ 𝑎 = 0 )) |
104 | 1, 24, 26, 80 | grpsubval 17465 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎(-g‘𝐺)𝑏) = (𝑎 + (𝐼‘𝑏))) |
105 | 104 | adantl 482 |
. . . . . 6
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(-g‘𝐺)𝑏) = (𝑎 + (𝐼‘𝑏))) |
106 | 105 | fveq2d 6195 |
. . . . 5
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎(-g‘𝐺)𝑏)) = (𝑁‘(𝑎 + (𝐼‘𝑏)))) |
107 | | 3simpc 1060 |
. . . . . . . . . 10
⊢ ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) |
108 | 107 | ralimi 2952 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) |
109 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
110 | 109 | ralimi 2952 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) |
111 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐼‘𝑏) → (𝑎 + 𝑦) = (𝑎 + (𝐼‘𝑏))) |
112 | 111 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐼‘𝑏) → (𝑁‘(𝑎 + 𝑦)) = (𝑁‘(𝑎 + (𝐼‘𝑏)))) |
113 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐼‘𝑏) → (𝑁‘𝑦) = (𝑁‘(𝐼‘𝑏))) |
114 | 113 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐼‘𝑏) → ((𝑁‘𝑎) + (𝑁‘𝑦)) = ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏)))) |
115 | 112, 114 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝐼‘𝑏) → ((𝑁‘(𝑎 + 𝑦)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑦)) ↔ (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏))))) |
116 | 94, 115 | rspc2v 3322 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝑋 ∧ (𝐼‘𝑏) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏))))) |
117 | 1, 26 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ 𝑏 ∈ 𝑋) → (𝐼‘𝑏) ∈ 𝑋) |
118 | 117 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 ∈ Grp → (𝑏 ∈ 𝑋 → (𝐼‘𝑏) ∈ 𝑋)) |
119 | 118 | anim2d 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ Grp → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎 ∈ 𝑋 ∧ (𝐼‘𝑏) ∈ 𝑋))) |
120 | 119 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎 ∈ 𝑋 ∧ (𝐼‘𝑏) ∈ 𝑋)) |
121 | 116, 120 | syl11 33 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) → ((𝐺 ∈ Grp ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏))))) |
122 | 121 | expd 452 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) → (𝐺 ∈ Grp → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏)))))) |
123 | 110, 122 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝐺 ∈ Grp → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏)))))) |
124 | 123 | imp 445 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏))))) |
125 | 124 | imp 445 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏)))) |
126 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥)) |
127 | 126 | ralimi 2952 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → ∀𝑥 ∈ 𝑋 (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥)) |
128 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑏 → (𝐼‘𝑥) = (𝐼‘𝑏)) |
129 | 128 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑏 → (𝑁‘(𝐼‘𝑥)) = (𝑁‘(𝐼‘𝑏))) |
130 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑏 → (𝑁‘𝑥) = (𝑁‘𝑏)) |
131 | 129, 130 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑏 → ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ↔ (𝑁‘(𝐼‘𝑏)) = (𝑁‘𝑏))) |
132 | 131 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑥 ∈
𝑋 (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝐼‘𝑏)) = (𝑁‘𝑏)) |
133 | 132 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝑋 (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ 𝑏 ∈ 𝑋) → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏))) |
134 | 133 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝑋 (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) → (𝑏 ∈ 𝑋 → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏)))) |
135 | 127, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝑏 ∈ 𝑋 → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏)))) |
136 | 135 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) → (𝑏 ∈ 𝑋 → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏)))) |
137 | 136 | adantld 483 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏)))) |
138 | 137 | imp 445 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘𝑏) = (𝑁‘(𝐼‘𝑏))) |
139 | 138 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑁‘𝑎) + (𝑁‘𝑏)) = ((𝑁‘𝑎) + (𝑁‘(𝐼‘𝑏)))) |
140 | 125, 139 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
141 | 140 | ex 450 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ 𝐺 ∈ Grp) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏)))) |
142 | 141 | ex 450 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 ((𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝐺 ∈ Grp → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))))) |
143 | 108, 142 | syl 17 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (𝐺 ∈ Grp → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))))) |
144 | 143 | impcom 446 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏)))) |
145 | 144 | adantl 482 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏)))) |
146 | 145 | imp 445 |
. . . . 5
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎 + (𝐼‘𝑏))) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
147 | 106, 146 | eqbrtrd 4675 |
. . . 4
⊢ (((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑁‘(𝑎(-g‘𝐺)𝑏)) ≤ ((𝑁‘𝑎) + (𝑁‘𝑏))) |
148 | 6, 1, 80, 42, 82, 83, 103, 147 | tngngpd 22457 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))) → 𝑇 ∈ NrmGrp) |
149 | 148 | ex 450 |
. 2
⊢ (𝑁:𝑋⟶ℝ → ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) → 𝑇 ∈ NrmGrp)) |
150 | 79, 149 | impbid 202 |
1
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ (𝑁‘(𝐼‘𝑥)) = (𝑁‘𝑥) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))) |