Metamath Proof Explorer

Theorem ngpinvds

Description: Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses ngpinvds.x ⊢ X = Base G
ngpinvds.i ⊢ I = inv g ⁡ G
ngpinvds.d ⊢ D = dist ⁡ G
Assertion ngpinvds ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ A D I ⁡ B = A D B

Proof

Step Hyp Ref Expression
1 ngpinvds.x ⊢ X = Base G
2 ngpinvds.i ⊢ I = inv g ⁡ G
3 ngpinvds.d ⊢ D = dist ⁡ G
4 eqid ⊢ - G = - G
5 simplr ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → G ∈ Abel
6 simprr ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → B ∈ X
7 simprl ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → A ∈ X
8 1 4 2 5 6 7 ablsub2inv ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ B - G I ⁡ A = A - G B
9 8 fveq2d ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → norm ⁡ G ⁡ I ⁡ B - G I ⁡ A = norm ⁡ G ⁡ A - G B
10 simpll ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → G ∈ NrmGrp
11 ngpgrp ⊢ G ∈ NrmGrp → G ∈ Grp
12 10 11 syl ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → G ∈ Grp
13 1 2 grpinvcl ⊢ G ∈ Grp ∧ A ∈ X → I ⁡ A ∈ X
14 12 7 13 syl2anc ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ A ∈ X
15 1 2 grpinvcl ⊢ G ∈ Grp ∧ B ∈ X → I ⁡ B ∈ X
16 12 6 15 syl2anc ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ B ∈ X
17 eqid ⊢ norm ⁡ G = norm ⁡ G
18 17 1 4 3 ngpdsr ⊢ G ∈ NrmGrp ∧ I ⁡ A ∈ X ∧ I ⁡ B ∈ X → I ⁡ A D I ⁡ B = norm ⁡ G ⁡ I ⁡ B - G I ⁡ A
19 10 14 16 18 syl3anc ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ A D I ⁡ B = norm ⁡ G ⁡ I ⁡ B - G I ⁡ A
20 17 1 4 3 ngpds ⊢ G ∈ NrmGrp ∧ A ∈ X ∧ B ∈ X → A D B = norm ⁡ G ⁡ A - G B
21 10 7 6 20 syl3anc ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → A D B = norm ⁡ G ⁡ A - G B
22 9 19 21 3eqtr4d ⊢ G ∈ NrmGrp ∧ G ∈ Abel ∧ A ∈ X ∧ B ∈ X → I ⁡ A D I ⁡ B = A D B