Proof of Theorem isngp3
Step | Hyp | Ref
| Expression |
1 | | isngp.n |
. . 3
⊢ 𝑁 = (norm‘𝐺) |
2 | | isngp.z |
. . 3
⊢ − =
(-g‘𝐺) |
3 | | isngp.d |
. . 3
⊢ 𝐷 = (dist‘𝐺) |
4 | | isngp2.x |
. . 3
⊢ 𝑋 = (Base‘𝐺) |
5 | | eqid 2622 |
. . 3
⊢ (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ↾ (𝑋 × 𝑋)) |
6 | 1, 2, 3, 4, 5 | isngp2 22401 |
. 2
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
7 | 4, 3 | msmet2 22265 |
. . . . . . . . 9
⊢ (𝐺 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
8 | 1, 4, 3, 5 | nmf2 22397 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) |
9 | 7, 8 | sylan2 491 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → 𝑁:𝑋⟶ℝ) |
10 | 4, 2 | grpsubf 17494 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
11 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → − :(𝑋 × 𝑋)⟶𝑋) |
12 | | fco 6058 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
13 | 9, 11, 12 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
14 | | ffn 6045 |
. . . . . . 7
⊢ ((𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ → (𝑁 ∘ − ) Fn (𝑋 × 𝑋)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ) Fn (𝑋 × 𝑋)) |
16 | 7 | adantl 482 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
17 | | metf 22135 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋) → (𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ) |
18 | | ffn 6045 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
20 | | eqfnov2 6767 |
. . . . . 6
⊢ (((𝑁 ∘ − ) Fn (𝑋 × 𝑋) ∧ (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
21 | 15, 19, 20 | syl2anc 693 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
22 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
23 | | fvco3 6275 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
24 | 11, 22, 23 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
25 | | df-ov 6653 |
. . . . . . . . 9
⊢ (𝑥(𝑁 ∘ − )𝑦) = ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) |
26 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝑥 − 𝑦) = ( − ‘〈𝑥, 𝑦〉) |
27 | 26 | fveq2i 6194 |
. . . . . . . . 9
⊢ (𝑁‘(𝑥 − 𝑦)) = (𝑁‘( − ‘〈𝑥, 𝑦〉)) |
28 | 24, 25, 27 | 3eqtr4g 2681 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑁 ∘ − )𝑦) = (𝑁‘(𝑥 − 𝑦))) |
29 | | ovres 6800 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
30 | 29 | adantl 482 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
31 | 28, 30 | eqeq12d 2637 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦))) |
32 | | eqcom 2629 |
. . . . . . 7
⊢ ((𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) |
33 | 31, 32 | syl6bb 276 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
34 | 33 | 2ralbidva 2988 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
35 | 21, 34 | bitrd 268 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
36 | 35 | pm5.32i 669 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
37 | | df-3an 1039 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
38 | | df-3an 1039 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
39 | 36, 37, 38 | 3bitr4i 292 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
40 | 6, 39 | bitri 264 |
1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |