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