Metamath Proof Explorer


Theorem nrgdsdir

Description: Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nmmul.x X = Base R
nmmul.n N = norm R
nmmul.t · ˙ = R
nrgdsdi.d D = dist R
Assertion nrgdsdir R NrmRing A X B X C X A D B N C = A · ˙ C D B · ˙ C

Proof

Step Hyp Ref Expression
1 nmmul.x X = Base R
2 nmmul.n N = norm R
3 nmmul.t · ˙ = R
4 nrgdsdi.d D = dist R
5 simpl R NrmRing A X B X C X R NrmRing
6 nrgring R NrmRing R Ring
7 6 adantr R NrmRing A X B X C X R Ring
8 ringgrp R Ring R Grp
9 7 8 syl R NrmRing A X B X C X R Grp
10 simpr1 R NrmRing A X B X C X A X
11 simpr2 R NrmRing A X B X C X B X
12 eqid - R = - R
13 1 12 grpsubcl R Grp A X B X A - R B X
14 9 10 11 13 syl3anc R NrmRing A X B X C X A - R B X
15 simpr3 R NrmRing A X B X C X C X
16 1 2 3 nmmul R NrmRing A - R B X C X N A - R B · ˙ C = N A - R B N C
17 5 14 15 16 syl3anc R NrmRing A X B X C X N A - R B · ˙ C = N A - R B N C
18 1 3 12 7 10 11 15 rngsubdir R NrmRing A X B X C X A - R B · ˙ C = A · ˙ C - R B · ˙ C
19 18 fveq2d R NrmRing A X B X C X N A - R B · ˙ C = N A · ˙ C - R B · ˙ C
20 17 19 eqtr3d R NrmRing A X B X C X N A - R B N C = N A · ˙ C - R B · ˙ C
21 nrgngp R NrmRing R NrmGrp
22 21 adantr R NrmRing A X B X C X R NrmGrp
23 2 1 12 4 ngpds R NrmGrp A X B X A D B = N A - R B
24 22 10 11 23 syl3anc R NrmRing A X B X C X A D B = N A - R B
25 24 oveq1d R NrmRing A X B X C X A D B N C = N A - R B N C
26 1 3 ringcl R Ring A X C X A · ˙ C X
27 7 10 15 26 syl3anc R NrmRing A X B X C X A · ˙ C X
28 1 3 ringcl R Ring B X C X B · ˙ C X
29 7 11 15 28 syl3anc R NrmRing A X B X C X B · ˙ C X
30 2 1 12 4 ngpds R NrmGrp A · ˙ C X B · ˙ C X A · ˙ C D B · ˙ C = N A · ˙ C - R B · ˙ C
31 22 27 29 30 syl3anc R NrmRing A X B X C X A · ˙ C D B · ˙ C = N A · ˙ C - R B · ˙ C
32 20 25 31 3eqtr4d R NrmRing A X B X C X A D B N C = A · ˙ C D B · ˙ C