nlmdsdir

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

	Ref	Expression
Hypotheses	nlmdsdi.v	$⊢ V = {Base}_{W}$
	nlmdsdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	nlmdsdi.f	$⊢ F = Scalar (W)$
	nlmdsdi.k	$⊢ K = {Base}_{F}$
	nlmdsdi.d	$⊢ D = dist (W)$
	nlmdsdir.n	$⊢ N = norm (W)$
	nlmdsdir.e	$⊢ E = dist (F)$
Assertion	nlmdsdir	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to (X E Y) N (Z) = (X \underset{˙}{\cdot} Z) D (Y \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		nlmdsdi.v	$⊢ V = {Base}_{W}$
2		nlmdsdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		nlmdsdi.f	$⊢ F = Scalar (W)$
4		nlmdsdi.k	$⊢ K = {Base}_{F}$
5		nlmdsdi.d	$⊢ D = dist (W)$
6		nlmdsdir.n	$⊢ N = norm (W)$
7		nlmdsdir.e	$⊢ E = dist (F)$
8		simpl	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to W \in NrmMod$
9	3	nlmngp2	$⊢ W \in NrmMod \to F \in NrmGrp$
10	9	adantr	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to F \in NrmGrp$
11		ngpgrp	$⊢ F \in NrmGrp \to F \in Grp$
12	10 11	syl	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to F \in Grp$
13		simpr1	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to X \in K$
14		simpr2	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to Y \in K$
15		eqid	$⊢ -_{F} = -_{F}$
16	4 15	grpsubcl	$⊢ (F \in Grp \land X \in K \land Y \in K) \to X -_{F} Y \in K$
17	12 13 14 16	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to X -_{F} Y \in K$
18		simpr3	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to Z \in V$
19		eqid	$⊢ norm (F) = norm (F)$
20	1 6 2 3 4 19	nmvs	$⊢ (W \in NrmMod \land X -_{F} Y \in K \land Z \in V) \to N ((X -_{F} Y) \underset{˙}{\cdot} Z) = norm (F) (X -_{F} Y) N (Z)$
21	8 17 18 20	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to N ((X -_{F} Y) \underset{˙}{\cdot} Z) = norm (F) (X -_{F} Y) N (Z)$
22		eqid	$⊢ -_{W} = -_{W}$
23		nlmlmod	$⊢ W \in NrmMod \to W \in LMod$
24	23	adantr	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to W \in LMod$
25	1 2 3 4 22 15 24 13 14 18	lmodsubdir	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to (X -_{F} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) -_{W} (Y \underset{˙}{\cdot} Z)$
26	25	fveq2d	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to N ((X -_{F} Y) \underset{˙}{\cdot} Z) = N ((X \underset{˙}{\cdot} Z) -_{W} (Y \underset{˙}{\cdot} Z))$
27	21 26	eqtr3d	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to norm (F) (X -_{F} Y) N (Z) = N ((X \underset{˙}{\cdot} Z) -_{W} (Y \underset{˙}{\cdot} Z))$
28	19 4 15 7	ngpds	$⊢ (F \in NrmGrp \land X \in K \land Y \in K) \to X E Y = norm (F) (X -_{F} Y)$
29	10 13 14 28	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to X E Y = norm (F) (X -_{F} Y)$
30	29	oveq1d	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to (X E Y) N (Z) = norm (F) (X -_{F} Y) N (Z)$
31		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
32	31	adantr	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to W \in NrmGrp$
33	1 3 2 4	lmodvscl	$⊢ (W \in LMod \land X \in K \land Z \in V) \to X \underset{˙}{\cdot} Z \in V$
34	24 13 18 33	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to X \underset{˙}{\cdot} Z \in V$
35	1 3 2 4	lmodvscl	$⊢ (W \in LMod \land Y \in K \land Z \in V) \to Y \underset{˙}{\cdot} Z \in V$
36	24 14 18 35	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to Y \underset{˙}{\cdot} Z \in V$
37	6 1 22 5	ngpds	$⊢ (W \in NrmGrp \land X \underset{˙}{\cdot} Z \in V \land Y \underset{˙}{\cdot} Z \in V) \to (X \underset{˙}{\cdot} Z) D (Y \underset{˙}{\cdot} Z) = N ((X \underset{˙}{\cdot} Z) -_{W} (Y \underset{˙}{\cdot} Z))$
38	32 34 36 37	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to (X \underset{˙}{\cdot} Z) D (Y \underset{˙}{\cdot} Z) = N ((X \underset{˙}{\cdot} Z) -_{W} (Y \underset{˙}{\cdot} Z))$
39	27 30 38	3eqtr4d	$⊢ (W \in NrmMod \land (X \in K \land Y \in K \land Z \in V)) \to (X E Y) N (Z) = (X \underset{˙}{\cdot} Z) D (Y \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem nlmdsdir

Proof