nrgdsdi

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	nrgdsdi	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to N (A) (B D C) = (A \underset{˙}{\cdot} B) D (A \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		simpr1	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to A \in X$
7		nrgring	$⊢ R \in NrmRing \to R \in Ring$
8	7	adantr	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to R \in Ring$
9		ringgrp	$⊢ R \in Ring \to R \in Grp$
10	8 9	syl	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to R \in Grp$
11		simpr2	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to B \in X$
12		simpr3	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to C \in X$
13		eqid	$⊢ -_{R} = -_{R}$
14	1 13	grpsubcl	$⊢ (R \in Grp \land B \in X \land C \in X) \to B -_{R} C \in X$
15	10 11 12 14	syl3anc	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to B -_{R} C \in X$
16	1 2 3	nmmul	$⊢ (R \in NrmRing \land A \in X \land B -_{R} C \in X) \to N (A \underset{˙}{\cdot} (B -_{R} C)) = N (A) N (B -_{R} C)$
17	5 6 15 16	syl3anc	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to N (A \underset{˙}{\cdot} (B -_{R} C)) = N (A) N (B -_{R} C)$
18	1 3 13 8 6 11 12	ringsubdi	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{\cdot} (B -_{R} C) = (A \underset{˙}{\cdot} B) -_{R} (A \underset{˙}{\cdot} C)$
19	18	fveq2d	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to N (A \underset{˙}{\cdot} (B -_{R} C)) = N ((A \underset{˙}{\cdot} B) -_{R} (A \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) N (B -_{R} C) = N ((A \underset{˙}{\cdot} B) -_{R} (A \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 13 4	ngpds	$⊢ (R \in NrmGrp \land B \in X \land C \in X) \to B D C = N (B -_{R} C)$
24	22 11 12 23	syl3anc	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to B D C = N (B -_{R} C)$
25	24	oveq2d	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to N (A) (B D C) = N (A) N (B -_{R} C)$
26	1 3	ringcl	$⊢ (R \in Ring \land A \in X \land B \in X) \to A \underset{˙}{\cdot} B \in X$
27	8 6 11 26	syl3anc	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{\cdot} B \in X$
28	1 3	ringcl	$⊢ (R \in Ring \land A \in X \land C \in X) \to A \underset{˙}{\cdot} C \in X$
29	8 6 12 28	syl3anc	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to A \underset{˙}{\cdot} C \in X$
30	2 1 13 4	ngpds	$⊢ (R \in NrmGrp \land A \underset{˙}{\cdot} B \in X \land A \underset{˙}{\cdot} C \in X) \to (A \underset{˙}{\cdot} B) D (A \underset{˙}{\cdot} C) = N ((A \underset{˙}{\cdot} B) -_{R} (A \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} B) D (A \underset{˙}{\cdot} C) = N ((A \underset{˙}{\cdot} B) -_{R} (A \underset{˙}{\cdot} C))$
32	20 25 31	3eqtr4d	$⊢ (R \in NrmRing \land (A \in X \land B \in X \land C \in X)) \to N (A) (B D C) = (A \underset{˙}{\cdot} B) D (A \underset{˙}{\cdot} C)$

Metamath Proof Explorer

Theorem nrgdsdi

Proof