Metamath Proof Explorer

Theorem nlmdsdir

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

Ref Expression
Hypotheses nlmdsdi.v 
|- V = ( Base ` W )
nlmdsdi.s 
|- .x. = ( .s ` W )
nlmdsdi.f 
|- F = ( Scalar ` W )
nlmdsdi.k 
|- K = ( Base ` F )
nlmdsdi.d 
|- D = ( dist ` W )
nlmdsdir.n 
|- N = ( norm ` W )
nlmdsdir.e 
|- E = ( dist ` F )
Assertion nlmdsdir 
|- ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X E Y ) x. ( N ` Z ) ) = ( ( X .x. Z ) D ( Y .x. Z ) ) )

Proof

Step Hyp Ref Expression
1 nlmdsdi.v 
 |-  V = ( Base ` W )
2 nlmdsdi.s 
 |-  .x. = ( .s ` W )
3 nlmdsdi.f 
 |-  F = ( Scalar ` W )
4 nlmdsdi.k 
 |-  K = ( Base ` F )
5 nlmdsdi.d 
 |-  D = ( dist ` W )
6 nlmdsdir.n 
 |-  N = ( norm ` W )
7 nlmdsdir.e 
 |-  E = ( dist ` F )
8 simpl 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> W e. NrmMod )
9 3 nlmngp2 
 |-  ( W e. NrmMod -> F e. NrmGrp )
10 9 adantr 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> F e. NrmGrp )
11 ngpgrp 
 |-  ( F e. NrmGrp -> F e. Grp )
12 10 11 syl 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> F e. Grp )
13 simpr1 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> X e. K )
14 simpr2 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> Y e. K )
15 eqid 
 |-  ( -g ` F ) = ( -g ` F )
16 4 15 grpsubcl 
 |-  ( ( F e. Grp /\ X e. K /\ Y e. K ) -> ( X ( -g ` F ) Y ) e. K )
17 12 13 14 16 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( X ( -g ` F ) Y ) e. K )
18 simpr3 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> Z e. V )
19 eqid 
 |-  ( norm ` F ) = ( norm ` F )
20 1 6 2 3 4 19 nmvs 
 |-  ( ( W e. NrmMod /\ ( X ( -g ` F ) Y ) e. K /\ Z e. V ) -> ( N ` ( ( X ( -g ` F ) Y ) .x. Z ) ) = ( ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) x. ( N ` Z ) ) )
21 8 17 18 20 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( N ` ( ( X ( -g ` F ) Y ) .x. Z ) ) = ( ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) x. ( N ` Z ) ) )
22 eqid 
 |-  ( -g ` W ) = ( -g ` W )
23 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
24 23 adantr 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> W e. LMod )
25 1 2 3 4 22 15 24 13 14 18 lmodsubdir 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X ( -g ` F ) Y ) .x. Z ) = ( ( X .x. Z ) ( -g ` W ) ( Y .x. Z ) ) )
26 25 fveq2d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( N ` ( ( X ( -g ` F ) Y ) .x. Z ) ) = ( N ` ( ( X .x. Z ) ( -g ` W ) ( Y .x. Z ) ) ) )
27 21 26 eqtr3d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) x. ( N ` Z ) ) = ( N ` ( ( X .x. Z ) ( -g ` W ) ( Y .x. Z ) ) ) )
28 19 4 15 7 ngpds 
 |-  ( ( F e. NrmGrp /\ X e. K /\ Y e. K ) -> ( X E Y ) = ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) )
29 10 13 14 28 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( X E Y ) = ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) )
30 29 oveq1d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X E Y ) x. ( N ` Z ) ) = ( ( ( norm ` F ) ` ( X ( -g ` F ) Y ) ) x. ( N ` Z ) ) )
31 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
32 31 adantr 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> W e. NrmGrp )
33 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ X e. K /\ Z e. V ) -> ( X .x. Z ) e. V )
34 24 13 18 33 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( X .x. Z ) e. V )
35 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ Y e. K /\ Z e. V ) -> ( Y .x. Z ) e. V )
36 24 14 18 35 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( Y .x. Z ) e. V )
37 6 1 22 5 ngpds 
 |-  ( ( W e. NrmGrp /\ ( X .x. Z ) e. V /\ ( Y .x. Z ) e. V ) -> ( ( X .x. Z ) D ( Y .x. Z ) ) = ( N ` ( ( X .x. Z ) ( -g ` W ) ( Y .x. Z ) ) ) )
38 32 34 36 37 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X .x. Z ) D ( Y .x. Z ) ) = ( N ` ( ( X .x. Z ) ( -g ` W ) ( Y .x. Z ) ) ) )
39 27 30 38 3eqtr4d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. K /\ Z e. V ) ) -> ( ( X E Y ) x. ( N ` Z ) ) = ( ( X .x. Z ) D ( Y .x. Z ) ) )