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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
ngpinvds.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
ngpinvds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion ngpinvds ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝐵 ) ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ngpinvds.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 ngpinvds.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
3 ngpinvds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
5 simplr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 ∈ Abel )
6 simprr ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
7 simprl ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
8 1 4 2 5 6 7 ablsub2inv ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐼 ‘ 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐼 ‘ 𝐴 ) ) = ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) )
9 8 fveq2d ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐼 ‘ 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐼 ‘ 𝐴 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) )
10 simpll ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 ∈ NrmGrp )
11 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
12 10 11 syl ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
13 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 )
14 12 7 13 syl2anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 )
15 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐵 ) ∈ 𝑋 )
16 12 6 15 syl2anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐼 ‘ 𝐵 ) ∈ 𝑋 )
17 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
18 17 1 4 3 ngpdsr ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐼 ‘ 𝐴 ) ∈ 𝑋 ∧ ( 𝐼 ‘ 𝐵 ) ∈ 𝑋 ) → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝐵 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐼 ‘ 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐼 ‘ 𝐴 ) ) ) )
19 10 14 16 18 syl3anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝐵 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐼 ‘ 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐼 ‘ 𝐴 ) ) ) )
20 17 1 4 3 ngpds ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) )
21 10 7 6 20 syl3anc ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) )
22 9 19 21 3eqtr4d ⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐼 ‘ 𝐴 ) 𝐷 ( 𝐼 ‘ 𝐵 ) ) = ( 𝐴 𝐷 𝐵 ) )