Proof of Theorem ngpocelbl
| Step | Hyp | Ref
| Expression |
| 1 | | nlmngp 24698 |
. . . . . . 7
⊢ (𝐺 ∈ NrmMod → 𝐺 ∈ NrmGrp) |
| 2 | | ngpocelbl.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 3 | | ngpocelbl.d |
. . . . . . . 8
⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) |
| 4 | 2, 3 | ngpmet 24616 |
. . . . . . 7
⊢ (𝐺 ∈ NrmGrp → 𝐷 ∈ (Met‘𝑋)) |
| 5 | | metxmet 24344 |
. . . . . . 7
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 6 | 1, 4, 5 | 3syl 18 |
. . . . . 6
⊢ (𝐺 ∈ NrmMod → 𝐷 ∈ (∞Met‘𝑋)) |
| 7 | 6 | anim1i 615 |
. . . . 5
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*)
→ (𝐷 ∈
(∞Met‘𝑋) ∧
𝑅 ∈
ℝ*)) |
| 8 | 7 | 3adant3 1133 |
. . . 4
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈
ℝ*)) |
| 9 | | simp3l 1202 |
. . . . 5
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝑃 ∈ 𝑋) |
| 10 | | ngpgrp 24612 |
. . . . . . . . 9
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) |
| 11 | 1, 10 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ NrmMod → 𝐺 ∈ Grp) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝐺 ∈ Grp) |
| 13 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) |
| 14 | | 3anass 1095 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ↔ (𝐺 ∈ Grp ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋))) |
| 15 | 12, 13, 14 | sylanbrc 583 |
. . . . . 6
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) |
| 16 | | ngpocelbl.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
| 17 | 2, 16 | grpcl 18959 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑃 + 𝐴) ∈ 𝑋) |
| 18 | 15, 17 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃 + 𝐴) ∈ 𝑋) |
| 19 | 9, 18 | jca 511 |
. . . 4
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋)) |
| 20 | 8, 19 | jca 511 |
. . 3
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋))) |
| 21 | | elbl2 24400 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋)) → ((𝑃 + 𝐴) ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷(𝑃 + 𝐴)) < 𝑅)) |
| 22 | 20, 21 | syl 17 |
. 2
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃 + 𝐴) ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷(𝑃 + 𝐴)) < 𝑅)) |
| 23 | 3 | oveqi 7444 |
. . . . . 6
⊢ (𝑃𝐷(𝑃 + 𝐴)) = (𝑃((dist‘𝐺) ↾ (𝑋 × 𝑋))(𝑃 + 𝐴)) |
| 24 | | ovres 7599 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋) → (𝑃((dist‘𝐺) ↾ (𝑋 × 𝑋))(𝑃 + 𝐴)) = (𝑃(dist‘𝐺)(𝑃 + 𝐴))) |
| 25 | 23, 24 | eqtrid 2789 |
. . . . 5
⊢ ((𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋) → (𝑃𝐷(𝑃 + 𝐴)) = (𝑃(dist‘𝐺)(𝑃 + 𝐴))) |
| 26 | 19, 25 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃𝐷(𝑃 + 𝐴)) = (𝑃(dist‘𝐺)(𝑃 + 𝐴))) |
| 27 | 1 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝐺 ∈ NrmGrp) |
| 28 | | ngpocelbl.n |
. . . . . 6
⊢ 𝑁 = (norm‘𝐺) |
| 29 | | eqid 2737 |
. . . . . 6
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 30 | | eqid 2737 |
. . . . . 6
⊢
(dist‘𝐺) =
(dist‘𝐺) |
| 31 | 28, 2, 29, 30 | ngpdsr 24618 |
. . . . 5
⊢ ((𝐺 ∈ NrmGrp ∧ 𝑃 ∈ 𝑋 ∧ (𝑃 + 𝐴) ∈ 𝑋) → (𝑃(dist‘𝐺)(𝑃 + 𝐴)) = (𝑁‘((𝑃 + 𝐴)(-g‘𝐺)𝑃))) |
| 32 | 27, 9, 18, 31 | syl3anc 1373 |
. . . 4
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃(dist‘𝐺)(𝑃 + 𝐴)) = (𝑁‘((𝑃 + 𝐴)(-g‘𝐺)𝑃))) |
| 33 | | nlmlmod 24699 |
. . . . . . . . 9
⊢ (𝐺 ∈ NrmMod → 𝐺 ∈ LMod) |
| 34 | | lmodabl 20907 |
. . . . . . . . 9
⊢ (𝐺 ∈ LMod → 𝐺 ∈ Abel) |
| 35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ NrmMod → 𝐺 ∈ Abel) |
| 36 | 35 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝐺 ∈ Abel) |
| 37 | | 3anass 1095 |
. . . . . . 7
⊢ ((𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ↔ (𝐺 ∈ Abel ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋))) |
| 38 | 36, 13, 37 | sylanbrc 583 |
. . . . . 6
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) |
| 39 | 2, 16, 29 | ablpncan2 19833 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑃 + 𝐴)(-g‘𝐺)𝑃) = 𝐴) |
| 40 | 38, 39 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃 + 𝐴)(-g‘𝐺)𝑃) = 𝐴) |
| 41 | 40 | fveq2d 6910 |
. . . 4
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑁‘((𝑃 + 𝐴)(-g‘𝐺)𝑃)) = (𝑁‘𝐴)) |
| 42 | 26, 32, 41 | 3eqtrd 2781 |
. . 3
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝑃𝐷(𝑃 + 𝐴)) = (𝑁‘𝐴)) |
| 43 | 42 | breq1d 5153 |
. 2
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃𝐷(𝑃 + 𝐴)) < 𝑅 ↔ (𝑁‘𝐴) < 𝑅)) |
| 44 | 22, 43 | bitrd 279 |
1
⊢ ((𝐺 ∈ NrmMod ∧ 𝑅 ∈ ℝ*
∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝑃 + 𝐴) ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑁‘𝐴) < 𝑅)) |