Metamath Proof Explorer

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 ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 𝐸 𝑌 ) · ( 𝑁 ‘ 𝑍 ) ) = ( ( 𝑋 · 𝑍 ) 𝐷 ( 𝑌 · 𝑍 ) ) )