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 2610 |
. . 3
⊢ (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ↾ (𝑋 × 𝑋)) |
6 | 1, 2, 3, 4, 5 | isngp2 22211 |
. 2
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
7 | 4, 3 | msmet2 22075 |
. . . . . . . . 9
⊢ (𝐺 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
8 | 1, 4, 3, 5 | nmf2 22207 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) |
9 | 7, 8 | sylan2 490 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → 𝑁:𝑋⟶ℝ) |
10 | 4, 2 | grpsubf 17317 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → − :(𝑋 × 𝑋)⟶𝑋) |
12 | | fco 5971 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
13 | 9, 11, 12 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
14 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ → (𝑁 ∘ − ) Fn (𝑋 × 𝑋)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ) Fn (𝑋 × 𝑋)) |
16 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
17 | | metf 21945 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋) → (𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ) |
18 | | ffn 5958 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
20 | | eqfnov2 6665 |
. . . . . 6
⊢ (((𝑁 ∘ − ) Fn (𝑋 × 𝑋) ∧ (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
21 | 15, 19, 20 | syl2anc 691 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
22 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
23 | | fvco3 6185 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
24 | 11, 22, 23 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
25 | | df-ov 6552 |
. . . . . . . . 9
⊢ (𝑥(𝑁 ∘ − )𝑦) = ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) |
26 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑥 − 𝑦) = ( − ‘〈𝑥, 𝑦〉) |
27 | 26 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝑁‘(𝑥 − 𝑦)) = (𝑁‘( − ‘〈𝑥, 𝑦〉)) |
28 | 24, 25, 27 | 3eqtr4g 2669 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑁 ∘ − )𝑦) = (𝑁‘(𝑥 − 𝑦))) |
29 | | ovres 6698 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
30 | 29 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
31 | 28, 30 | eqeq12d 2625 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦))) |
32 | | eqcom 2617 |
. . . . . . 7
⊢ ((𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) |
33 | 31, 32 | syl6bb 275 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
34 | 33 | 2ralbidva 2971 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
35 | 21, 34 | bitrd 267 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
36 | 35 | pm5.32i 667 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
37 | | df-3an 1033 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
38 | | df-3an 1033 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
39 | 36, 37, 38 | 3bitr4i 291 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
40 | 6, 39 | bitri 263 |
1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |