Proof of Theorem isngp4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ngpgrp 24612 | . . 3
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) | 
| 2 |  | ngpms 24613 | . . 3
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) | 
| 3 |  | ngprcan.x | . . . . 5
⊢ 𝑋 = (Base‘𝐺) | 
| 4 |  | ngprcan.p | . . . . 5
⊢  + =
(+g‘𝐺) | 
| 5 |  | ngprcan.d | . . . . 5
⊢ 𝐷 = (dist‘𝐺) | 
| 6 | 3, 4, 5 | ngprcan 24623 | . . . 4
⊢ ((𝐺 ∈ NrmGrp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) | 
| 7 | 6 | ralrimivvva 3205 | . . 3
⊢ (𝐺 ∈ NrmGrp →
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) | 
| 8 | 1, 2, 7 | 3jca 1129 | . 2
⊢ (𝐺 ∈ NrmGrp → (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦))) | 
| 9 |  | simp1 1137 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ Grp) | 
| 10 |  | simp2 1138 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ MetSp) | 
| 11 |  | eqid 2737 | . . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 12 | 3, 11 | grpinvcl 19005 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) | 
| 13 | 12 | ad2ant2rl 749 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ 𝑋) | 
| 14 |  | eqcom 2744 | . . . . . . . . 9
⊢ (((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧))) | 
| 15 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (𝑥 + 𝑧) = (𝑥 +
((invg‘𝐺)‘𝑦))) | 
| 16 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (𝑦 + 𝑧) = (𝑦 +
((invg‘𝐺)‘𝑦))) | 
| 17 | 15, 16 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦)))) | 
| 18 | 17 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → ((𝑥𝐷𝑦) = ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) ↔ (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) | 
| 19 | 14, 18 | bitrid 283 | . . . . . . . 8
⊢ (𝑧 = ((invg‘𝐺)‘𝑦) → (((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) ↔ (𝑥𝐷𝑦) = ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))))) | 
| 20 | 19 | rspcv 3618 | . . . . . . 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 19003 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(-g‘𝐺)𝑦) = (𝑥 +
((invg‘𝐺)‘𝑦))) | 
| 24 | 23 | adantl 481 | . . . . . . . . . 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 19008 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋) → (𝑦 +
((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) | 
| 28 | 27 | ad2ant2rl 749 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 +
((invg‘𝐺)‘𝑦)) = (0g‘𝐺)) | 
| 29 | 25, 28 | oveq12d 7449 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 +
((invg‘𝐺)‘𝑦))𝐷(𝑦 +
((invg‘𝐺)‘𝑦))) = ((𝑥(-g‘𝐺)𝑦)𝐷(0g‘𝐺))) | 
| 30 | 3, 22 | grpsubcl 19038 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) | 
| 31 | 30 | 3expb 1121 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) | 
| 32 | 31 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑋) | 
| 33 |  | eqid 2737 | . . . . . . . . . 10
⊢
(norm‘𝐺) =
(norm‘𝐺) | 
| 34 | 33, 3, 26, 5 | nmval 24602 | . . . . . . . . 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 239 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) | 
| 39 | 38 | ralimdvva 3206 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) →
(∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) | 
| 40 | 39 | 3impia 1118 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) | 
| 41 | 33, 22, 5, 3 | isngp3 24611 | . . 3
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)))) | 
| 42 | 9, 10, 40, 41 | syl3anbrc 1344 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦)) → 𝐺 ∈ NrmGrp) | 
| 43 | 8, 42 | impbii 209 | 1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥 + 𝑧)𝐷(𝑦 + 𝑧)) = (𝑥𝐷𝑦))) |