Theorem nlmdsdir

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

	Ref	Expression
Hypotheses	nlmdsdi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	nlmdsdi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	nlmdsdi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	nlmdsdi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	nlmdsdi.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
	nlmdsdir.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	nlmdsdir.e	⊢ 𝐸 = ( dist ‘ 𝐹 )
Assertion	nlmdsdir	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 𝐸 𝑌 ) · ( 𝑁 ‘ 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) 𝐷 ( 𝑌 · 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nlmdsdi.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		nlmdsdi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		nlmdsdi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		nlmdsdi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		nlmdsdi.d	⊢ 𝐷 = ( dist ‘ 𝑊 )
6		nlmdsdir.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
7		nlmdsdir.e	⊢ 𝐸 = ( dist ‘ 𝐹 )
8		simpl	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ NrmMod )
9	3	nlmngp2	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
10	9	adantr	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝐹 ∈ NrmGrp )
11		ngpgrp	⊢ ( 𝐹 ∈ NrmGrp → 𝐹 ∈ Grp )
12	10 11	syl	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝐹 ∈ Grp )
13		simpr1	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑋 ∈ 𝐾 )
14		simpr2	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑌 ∈ 𝐾 )
15		eqid	⊢ ( -g ‘ 𝐹 ) = ( -g ‘ 𝐹 )
16	4 15	grpsubcl	⊢ ( ( 𝐹 ∈ Grp ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ∈ 𝐾 )
17	12 13 14 16	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ∈ 𝐾 )
18		simpr3	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
19		eqid	⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
20	1 6 2 3 4 19	nmvs	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ ( ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) · 𝑍 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) · ( 𝑁 ‘ 𝑍 ) ) )
21	8 17 18 20	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) · 𝑍 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) · ( 𝑁 ‘ 𝑍 ) ) )
22		eqid	⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
23		nlmlmod	⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
24	23	adantr	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
25	1 2 3 4 22 15 24 13 14 18	lmodsubdir	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) ( -g ‘ 𝑊 ) ( 𝑌 · 𝑍 ) ) )
26	25	fveq2d	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑁 ‘ ( ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) · 𝑍 ) ) = ( 𝑁 ‘ ( ( 𝑋 · 𝑍 ) ( -g ‘ 𝑊 ) ( 𝑌 · 𝑍 ) ) ) )
27	21 26	eqtr3d	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) · ( 𝑁 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( ( 𝑋 · 𝑍 ) ( -g ‘ 𝑊 ) ( 𝑌 · 𝑍 ) ) ) )
28	19 4 15 7	ngpds	⊢ ( ( 𝐹 ∈ NrmGrp ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 𝐸 𝑌 ) = ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) )
29	10 13 14 28	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 𝐸 𝑌 ) = ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) )
30	29	oveq1d	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 𝐸 𝑌 ) · ( 𝑁 ‘ 𝑍 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ ( 𝑋 ( -g ‘ 𝐹 ) 𝑌 ) ) · ( 𝑁 ‘ 𝑍 ) ) )
31		nlmngp	⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
32	31	adantr	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ NrmGrp )
33	1 3 2 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑋 · 𝑍 ) ∈ 𝑉 )
34	24 13 18 33	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 · 𝑍 ) ∈ 𝑉 )
35	1 3 2 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 · 𝑍 ) ∈ 𝑉 )
36	24 14 18 35	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑌 · 𝑍 ) ∈ 𝑉 )
37	6 1 22 5	ngpds	⊢ ( ( 𝑊 ∈ NrmGrp ∧ ( 𝑋 · 𝑍 ) ∈ 𝑉 ∧ ( 𝑌 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑋 · 𝑍 ) 𝐷 ( 𝑌 · 𝑍 ) ) = ( 𝑁 ‘ ( ( 𝑋 · 𝑍 ) ( -g ‘ 𝑊 ) ( 𝑌 · 𝑍 ) ) ) )
38	32 34 36 37	syl3anc	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑍 ) 𝐷 ( 𝑌 · 𝑍 ) ) = ( 𝑁 ‘ ( ( 𝑋 · 𝑍 ) ( -g ‘ 𝑊 ) ( 𝑌 · 𝑍 ) ) ) )
39	27 30 38	3eqtr4d	⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 𝐸 𝑌 ) · ( 𝑁 ‘ 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) 𝐷 ( 𝑌 · 𝑍 ) ) )