Theorem ngplcan

Description: Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	ngprcan.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ngprcan.p	⊢ + = ( +g ‘ 𝐺 )
	ngprcan.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion	ngplcan	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 + 𝐴 ) 𝐷 ( 𝐶 + 𝐵 ) ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ngprcan.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		ngprcan.p	⊢ + = ( +g ‘ 𝐺 )
3		ngprcan.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
4		simplr	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ Abel )
5		simpr3	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
6		simpr1	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
7	1 2	ablcom	⊢ ( ( 𝐺 ∈ Abel ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 + 𝐴 ) = ( 𝐴 + 𝐶 ) )
8	4 5 6 7	syl3anc	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 + 𝐴 ) = ( 𝐴 + 𝐶 ) )
9		simpr2	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
10	1 2	ablcom	⊢ ( ( 𝐺 ∈ Abel ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
11	4 5 9 10	syl3anc	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
12	8 11	oveq12d	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 + 𝐴 ) 𝐷 ( 𝐶 + 𝐵 ) ) = ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) )
13	1 2 3	ngprcan	⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )
14	13	adantlr	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )
15	12 14	eqtrd	⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 + 𝐴 ) 𝐷 ( 𝐶 + 𝐵 ) ) = ( 𝐴 𝐷 𝐵 ) )