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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) )