Metamath Proof Explorer


Theorem ngprcan

Description: Cancel right 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 ngprcan ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ngprcan.x 𝑋 = ( Base ‘ 𝐺 )
2 ngprcan.p + = ( +g𝐺 )
3 ngprcan.d 𝐷 = ( dist ‘ 𝐺 )
4 ngpgrp ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5 eqid ( -g𝐺 ) = ( -g𝐺 )
6 1 2 5 grppnpcan2 ( ( 𝐺 ∈ Grp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 + 𝐶 ) ( -g𝐺 ) ( 𝐵 + 𝐶 ) ) = ( 𝐴 ( -g𝐺 ) 𝐵 ) )
7 4 6 sylan ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 + 𝐶 ) ( -g𝐺 ) ( 𝐵 + 𝐶 ) ) = ( 𝐴 ( -g𝐺 ) 𝐵 ) )
8 7 fveq2d ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐴 + 𝐶 ) ( -g𝐺 ) ( 𝐵 + 𝐶 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g𝐺 ) 𝐵 ) ) )
9 simpl ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐺 ∈ NrmGrp )
10 4 adantr ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐺 ∈ Grp )
11 simpr1 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐴𝑋 )
12 simpr3 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐶𝑋 )
13 1 2 grpcl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 + 𝐶 ) ∈ 𝑋 )
14 10 11 12 13 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 + 𝐶 ) ∈ 𝑋 )
15 simpr2 ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 𝐵𝑋 )
16 1 2 grpcl ( ( 𝐺 ∈ Grp ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
17 10 15 12 16 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
18 eqid ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
19 18 1 5 3 ngpds ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 + 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 + 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐴 + 𝐶 ) ( -g𝐺 ) ( 𝐵 + 𝐶 ) ) ) )
20 9 14 17 19 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( ( norm ‘ 𝐺 ) ‘ ( ( 𝐴 + 𝐶 ) ( -g𝐺 ) ( 𝐵 + 𝐶 ) ) ) )
21 18 1 5 3 ngpds ( ( 𝐺 ∈ NrmGrp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g𝐺 ) 𝐵 ) ) )
22 9 11 15 21 syl3anc ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝐴 ( -g𝐺 ) 𝐵 ) ) )
23 8 20 22 3eqtr4d ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )