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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	nrgdsdi.d	$⊢ D = dist (R)$
Assertion	nrgdsdir	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to (A D B) N (C) = (A \underset{˙}{\cdot} C) D (B \underset{˙}{\cdot} C)$

Proof

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

Metamath Proof Explorer

Theorem nrgdsdir

Proof