nlmdsdi

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)$
	nlmdsdi.a	$⊢ A = norm (F)$
Assertion	nlmdsdi	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to A (X) (Y D Z) = (X \underset{˙}{\cdot} Y) D (X \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		nlmdsdi.a	$⊢ A = norm (F)$
7		simpl	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to W \in NrmMod$
8		simpr1	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to X \in K$
9		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
10	9	adantr	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to W \in NrmGrp$
11		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
12	10 11	syl	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to W \in Grp$
13		simpr2	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to Y \in V$
14		simpr3	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to Z \in V$
15		eqid	$⊢ -_{W} = -_{W}$
16	1 15	grpsubcl	$⊢ (W \in Grp \land Y \in V \land Z \in V) \to Y -_{W} Z \in V$
17	12 13 14 16	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to Y -_{W} Z \in V$
18		eqid	$⊢ norm (W) = norm (W)$
19	1 18 2 3 4 6	nmvs	$⊢ (W \in NrmMod \land X \in K \land Y -_{W} Z \in V) \to norm (W) (X \underset{˙}{\cdot} (Y -_{W} Z)) = A (X) norm (W) (Y -_{W} Z)$
20	7 8 17 19	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to norm (W) (X \underset{˙}{\cdot} (Y -_{W} Z)) = A (X) norm (W) (Y -_{W} Z)$
21		nlmlmod	$⊢ W \in NrmMod \to W \in LMod$
22	21	adantr	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to W \in LMod$
23	1 2 3 4 15 22 8 13 14	lmodsubdi	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to X \underset{˙}{\cdot} (Y -_{W} Z) = (X \underset{˙}{\cdot} Y) -_{W} (X \underset{˙}{\cdot} Z)$
24	23	fveq2d	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to norm (W) (X \underset{˙}{\cdot} (Y -_{W} Z)) = norm (W) ((X \underset{˙}{\cdot} Y) -_{W} (X \underset{˙}{\cdot} Z))$
25	20 24	eqtr3d	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to A (X) norm (W) (Y -_{W} Z) = norm (W) ((X \underset{˙}{\cdot} Y) -_{W} (X \underset{˙}{\cdot} Z))$
26	18 1 15 5	ngpds	$⊢ (W \in NrmGrp \land Y \in V \land Z \in V) \to Y D Z = norm (W) (Y -_{W} Z)$
27	10 13 14 26	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to Y D Z = norm (W) (Y -_{W} Z)$
28	27	oveq2d	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to A (X) (Y D Z) = A (X) norm (W) (Y -_{W} Z)$
29	1 3 2 4	lmodvscl	$⊢ (W \in LMod \land X \in K \land Y \in V) \to X \underset{˙}{\cdot} Y \in V$
30	22 8 13 29	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to X \underset{˙}{\cdot} Y \in V$
31	1 3 2 4	lmodvscl	$⊢ (W \in LMod \land X \in K \land Z \in V) \to X \underset{˙}{\cdot} Z \in V$
32	22 8 14 31	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to X \underset{˙}{\cdot} Z \in V$
33	18 1 15 5	ngpds	$⊢ (W \in NrmGrp \land X \underset{˙}{\cdot} Y \in V \land X \underset{˙}{\cdot} Z \in V) \to (X \underset{˙}{\cdot} Y) D (X \underset{˙}{\cdot} Z) = norm (W) ((X \underset{˙}{\cdot} Y) -_{W} (X \underset{˙}{\cdot} Z))$
34	10 30 32 33	syl3anc	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to (X \underset{˙}{\cdot} Y) D (X \underset{˙}{\cdot} Z) = norm (W) ((X \underset{˙}{\cdot} Y) -_{W} (X \underset{˙}{\cdot} Z))$
35	25 28 34	3eqtr4d	$⊢ (W \in NrmMod \land (X \in K \land Y \in V \land Z \in V)) \to A (X) (Y D Z) = (X \underset{˙}{\cdot} Y) D (X \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem nlmdsdi

Proof