This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ngpsubcan

Description: Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses ngpsubcan.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ngpsubcan.m ⊢ − = ( -g ‘ 𝐺 )
ngpsubcan.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion ngpsubcan ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 − 𝐶 ) 𝐷 ( 𝐵 − 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ngpsubcan.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 ngpsubcan.m ⊢ − = ( -g ‘ 𝐺 )
3 ngpsubcan.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 simpr1 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
5 simpr3 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
8 1 6 7 2 grpsubval ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 − 𝐶 ) = ( 𝐴 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) )
9 4 5 8 syl2anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 − 𝐶 ) = ( 𝐴 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) )
10 simpr2 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
11 1 6 7 2 grpsubval ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 − 𝐶 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) )
12 10 5 11 syl2anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 − 𝐶 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) )
13 9 12 oveq12d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 − 𝐶 ) 𝐷 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) 𝐷 ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) ) )
14 simpl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ NrmGrp )
15 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
16 1 7 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
17 15 5 16 syl2an2r ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
18 1 6 3 ngprcan ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) 𝐷 ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) ) = ( 𝐴 𝐷 𝐵 ) )
19 14 4 10 17 18 syl13anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) 𝐷 ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ) ) = ( 𝐴 𝐷 𝐵 ) )
20 13 19 eqtrd ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 − 𝐶 ) 𝐷 ( 𝐵 − 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )