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=BaseG
ngpinvds.i ⊢I=invg⁡G
ngpinvds.d ⊢D=dist⁡G
Assertion ngpinvds ⊢G∈NrmGrp∧G∈Abel∧A∈X∧B∈X→I⁡ADI⁡B=ADB

Proof

Step Hyp Ref Expression
1 ngpinvds.x ⊢X=BaseG
2 ngpinvds.i ⊢I=invg⁡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-GI⁡A=A-GB
9 8 fveq2d ⊢G∈NrmGrp∧G∈Abel∧A∈X∧B∈X→norm⁡G⁡I⁡B-GI⁡A=norm⁡G⁡A-GB
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⁡ADI⁡B=norm⁡G⁡I⁡B-GI⁡A
19 10 14 16 18 syl3anc ⊢G∈NrmGrp∧G∈Abel∧A∈X∧B∈X→I⁡ADI⁡B=norm⁡G⁡I⁡B-GI⁡A
20 17 1 4 3 ngpds ⊢G∈NrmGrp∧A∈X∧B∈X→ADB=norm⁡G⁡A-GB
21 10 7 6 20 syl3anc ⊢G∈NrmGrp∧G∈Abel∧A∈X∧B∈X→ADB=norm⁡G⁡A-GB
22 9 19 21 3eqtr4d ⊢G∈NrmGrp∧G∈Abel∧A∈X∧B∈X→I⁡ADI⁡B=ADB