Metamath Proof Explorer

Theorem nlmdsdi

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 ‘ 𝑊 )
nlmdsdi.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
Assertion nlmdsdi ( ( 𝑊 ∈ 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 nlmdsdi.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
7 simpl ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ NrmMod )
8 simpr1 ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑋 ∈ 𝐾 )
9 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
10 9 adantr ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ NrmGrp )
11 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
12 10 11 syl ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ Grp )
13 simpr2 ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑌 ∈ 𝑉 )
14 simpr3 ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
15 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
16 1 15 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
17 12 13 14 16 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
18 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
19 1 18 2 3 4 6 nmvs ⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝑋 · ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) )
20 7 8 17 19 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝑋 · ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) )
21 nlmlmod ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
22 21 adantr ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
23 1 2 3 4 15 22 8 13 14 lmodsubdi ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 · ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 · 𝑍 ) ) )
24 23 fveq2d ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝑋 · ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) = ( ( norm ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 · 𝑍 ) ) ) )
25 20 24 eqtr3d ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝐴 ‘ 𝑋 ) · ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) = ( ( norm ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 · 𝑍 ) ) ) )
26 18 1 15 5 ngpds ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 𝐷 𝑍 ) = ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) )
27 10 13 14 26 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑌 𝐷 𝑍 ) = ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) )
28 27 oveq2d ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝐴 ‘ 𝑋 ) · ( 𝑌 𝐷 𝑍 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( ( norm ‘ 𝑊 ) ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑍 ) ) ) )
29 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 · 𝑌 ) ∈ 𝑉 )
30 22 8 13 29 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑉 )
31 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑋 · 𝑍 ) ∈ 𝑉 )
32 22 8 14 31 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( 𝑋 · 𝑍 ) ∈ 𝑉 )
33 18 1 15 5 ngpds ⊢ ( ( 𝑊 ∈ NrmGrp ∧ ( 𝑋 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑋 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑋 · 𝑌 ) 𝐷 ( 𝑋 · 𝑍 ) ) = ( ( norm ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 · 𝑍 ) ) ) )
34 10 30 32 33 syl3anc ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝑋 · 𝑌 ) 𝐷 ( 𝑋 · 𝑍 ) ) = ( ( norm ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑊 ) ( 𝑋 · 𝑍 ) ) ) )
35 25 28 34 3eqtr4d ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝐴 ‘ 𝑋 ) · ( 𝑌 𝐷 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) 𝐷 ( 𝑋 · 𝑍 ) ) )