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 2737 |
. . 3
⊢ (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ↾ (𝑋 × 𝑋)) |
| 6 | 1, 2, 3, 4, 5 | isngp2 24610 |
. 2
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
| 7 | 4, 3 | msmet2 24470 |
. . . . . . . . 9
⊢ (𝐺 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
| 8 | 1, 4, 3, 5 | nmf2 24606 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) |
| 9 | 7, 8 | sylan2 593 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → 𝑁:𝑋⟶ℝ) |
| 10 | 4, 2 | grpsubf 19037 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → − :(𝑋 × 𝑋)⟶𝑋) |
| 12 | | fco 6760 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
| 13 | 9, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
| 14 | 13 | ffnd 6737 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝑁 ∘ − ) Fn (𝑋 × 𝑋)) |
| 15 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
| 16 | | metf 24340 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋) → (𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ) |
| 17 | | ffn 6736 |
. . . . . . 7
⊢ ((𝐷 ↾ (𝑋 × 𝑋)):(𝑋 × 𝑋)⟶ℝ → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
| 18 | 15, 16, 17 | 3syl 18 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) |
| 19 | | eqfnov2 7563 |
. . . . . 6
⊢ (((𝑁 ∘ − ) Fn (𝑋 × 𝑋) ∧ (𝐷 ↾ (𝑋 × 𝑋)) Fn (𝑋 × 𝑋)) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
| 20 | 14, 18, 19 | syl2anc 584 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦))) |
| 21 | | opelxpi 5722 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) |
| 22 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (( − :(𝑋 × 𝑋)⟶𝑋 ∧ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
| 23 | 11, 21, 22 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) = (𝑁‘( − ‘〈𝑥, 𝑦〉))) |
| 24 | | df-ov 7434 |
. . . . . . . . 9
⊢ (𝑥(𝑁 ∘ − )𝑦) = ((𝑁 ∘ − )‘〈𝑥, 𝑦〉) |
| 25 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑥 − 𝑦) = ( − ‘〈𝑥, 𝑦〉) |
| 26 | 25 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝑁‘(𝑥 − 𝑦)) = (𝑁‘( − ‘〈𝑥, 𝑦〉)) |
| 27 | 23, 24, 26 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝑁 ∘ − )𝑦) = (𝑁‘(𝑥 − 𝑦))) |
| 28 | | ovres 7599 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
| 29 | 28 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) = (𝑥𝐷𝑦)) |
| 30 | 27, 29 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦))) |
| 31 | | eqcom 2744 |
. . . . . . 7
⊢ ((𝑁‘(𝑥 − 𝑦)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) |
| 32 | 30, 31 | bitrdi 287 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 33 | 32 | 2ralbidva 3219 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥(𝑁 ∘ − )𝑦) = (𝑥(𝐷 ↾ (𝑋 × 𝑋))𝑦) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 34 | 20, 33 | bitrd 279 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 35 | 34 | pm5.32i 574 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 36 | | df-3an 1089 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋)))) |
| 37 | | df-3an 1089 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦))) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 38 | 35, 36, 37 | 3bitr4i 303 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = (𝐷 ↾ (𝑋 × 𝑋))) ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |
| 39 | 6, 38 | bitri 275 |
1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) |