Proof of Theorem isngp4
Step | Hyp | Ref
| Expression |
1 | | ngpgrp 23497 |
. . 3
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) |
2 | | ngpms 23498 |
. . 3
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) |
3 | | ngprcan.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
4 | | ngprcan.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
5 | | ngprcan.d |
. . . . 5
⊢ 𝐷 = (dist‘𝐺) |
6 | 3, 4, 5 | ngprcan 23508 |
. . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) |
7 | 6 | ralrimivvva 3113 |
. . 3
⊢ (𝐺 ∈ NrmGrp →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) |
8 | 1, 2, 7 | 3jca 1130 |
. 2
⊢ (𝐺 ∈ NrmGrp → (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦))) |
9 | | simp1 1138 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ Grp) |
10 | | simp2 1139 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ MetSp) |
11 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) |
12 | 3, 11 | grpinvcl 18415 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
13 | 12 | ad2ant2rl 749 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) |
14 | | eqcom 2744 |
. . . . . . . . 9
⊢ (((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧))) |
15 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (𝑥 + 𝑧) = (𝑥 +
((invg‘𝐺)‘𝑦))) |
16 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (𝑦 + 𝑧) = (𝑦 +
((invg‘𝐺)‘𝑦))) |
17 | 15, 16 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦)))) |
18 | 17 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → ((𝑥𝐷𝑦) = ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) ↔ (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) |
19 | 14, 18 | syl5bb 286 |
. . . . . . . 8
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) |
20 | 19 | rspcv 3532 |
. . . . . . 7
⊢
(((invg‘𝐺)‘𝑦) ∈ 𝑋 → (∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) |
21 | 13, 20 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) |
22 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(-g‘𝐺) = (-g‘𝐺) |
23 | 3, 4, 11, 22 | grpsubval 18413 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(-g‘𝐺)𝑦) = (𝑥 +
((invg‘𝐺)‘𝑦))) |
24 | 23 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(-g‘𝐺)𝑦) = (𝑥 +
((invg‘𝐺)‘𝑦))) |
25 | 24 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 +
((invg‘𝐺)‘𝑦)) = (𝑥(-g‘𝐺)𝑦)) |
26 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) = (0g‘𝐺) |
27 | 3, 4, 26, 11 | grprinv 18417 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦 +
((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
28 | 27 | ad2ant2rl 749 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 +
((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) |
29 | 25, 28 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))) = ((𝑥(-g‘𝐺)𝑦)𝐷(0g‘𝐺))) |
30 | 3, 22 | grpsubcl 18443 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) |
31 | 30 | 3expb 1122 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) |
32 | 31 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) |
33 | | eqid 2737 |
. . . . . . . . . 10
⊢
(norm‘𝐺) =
(norm‘𝐺) |
34 | 33, 3, 26, 5 | nmval 23487 |
. . . . . . . . 9
⊢ ((𝑥(-g‘𝐺)𝑦) ∈ 𝑋 → ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)) = ((𝑥(-g‘𝐺)𝑦)𝐷(0g‘𝐺))) |
35 | 32, 34 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)) = ((𝑥(-g‘𝐺)𝑦)𝐷(0g‘𝐺))) |
36 | 29, 35 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) |
37 | 36 | eqeq2d 2748 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))) ↔ (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) |
38 | 21, 37 | sylibd 242 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) |
39 | 38 | ralimdvva 3102 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) |
40 | 39 | 3impia 1119 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) |
41 | 33, 22, 5, 3 | isngp3 23496 |
. . 3
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) |
42 | 9, 10, 40, 41 | syl3anbrc 1345 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ NrmGrp) |
43 | 8, 42 | impbii 212 |
1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦))) |