Metamath Proof Explorer

Theorem nlmdsdi

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 )
nlmdsdi.a 
|- A = ( norm ` F )
Assertion nlmdsdi 
|- ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( A ` X ) x. ( Y D Z ) ) = ( ( X .x. Y ) D ( X .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 nlmdsdi.a 
 |-  A = ( norm ` F )
7 simpl 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> W e. NrmMod )
8 simpr1 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> X e. K )
9 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
10 9 adantr 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> W e. NrmGrp )
11 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
12 10 11 syl 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> W e. Grp )
13 simpr2 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> Y e. V )
14 simpr3 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> Z e. V )
15 eqid 
 |-  ( -g ` W ) = ( -g ` W )
16 1 15 grpsubcl 
 |-  ( ( W e. Grp /\ Y e. V /\ Z e. V ) -> ( Y ( -g ` W ) Z ) e. V )
17 12 13 14 16 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( Y ( -g ` W ) Z ) e. V )
18 eqid 
 |-  ( norm ` W ) = ( norm ` W )
19 1 18 2 3 4 6 nmvs 
 |-  ( ( W e. NrmMod /\ X e. K /\ ( Y ( -g ` W ) Z ) e. V ) -> ( ( norm ` W ) ` ( X .x. ( Y ( -g ` W ) Z ) ) ) = ( ( A ` X ) x. ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) ) )
20 7 8 17 19 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( norm ` W ) ` ( X .x. ( Y ( -g ` W ) Z ) ) ) = ( ( A ` X ) x. ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) ) )
21 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
22 21 adantr 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> W e. LMod )
23 1 2 3 4 15 22 8 13 14 lmodsubdi 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( X .x. ( Y ( -g ` W ) Z ) ) = ( ( X .x. Y ) ( -g ` W ) ( X .x. Z ) ) )
24 23 fveq2d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( norm ` W ) ` ( X .x. ( Y ( -g ` W ) Z ) ) ) = ( ( norm ` W ) ` ( ( X .x. Y ) ( -g ` W ) ( X .x. Z ) ) ) )
25 20 24 eqtr3d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( A ` X ) x. ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) ) = ( ( norm ` W ) ` ( ( X .x. Y ) ( -g ` W ) ( X .x. Z ) ) ) )
26 18 1 15 5 ngpds 
 |-  ( ( W e. NrmGrp /\ Y e. V /\ Z e. V ) -> ( Y D Z ) = ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) )
27 10 13 14 26 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( Y D Z ) = ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) )
28 27 oveq2d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( A ` X ) x. ( Y D Z ) ) = ( ( A ` X ) x. ( ( norm ` W ) ` ( Y ( -g ` W ) Z ) ) ) )
29 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ X e. K /\ Y e. V ) -> ( X .x. Y ) e. V )
30 22 8 13 29 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( X .x. Y ) e. V )
31 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ X e. K /\ Z e. V ) -> ( X .x. Z ) e. V )
32 22 8 14 31 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( X .x. Z ) e. V )
33 18 1 15 5 ngpds 
 |-  ( ( W e. NrmGrp /\ ( X .x. Y ) e. V /\ ( X .x. Z ) e. V ) -> ( ( X .x. Y ) D ( X .x. Z ) ) = ( ( norm ` W ) ` ( ( X .x. Y ) ( -g ` W ) ( X .x. Z ) ) ) )
34 10 30 32 33 syl3anc 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( X .x. Y ) D ( X .x. Z ) ) = ( ( norm ` W ) ` ( ( X .x. Y ) ( -g ` W ) ( X .x. Z ) ) ) )
35 25 28 34 3eqtr4d 
 |-  ( ( W e. NrmMod /\ ( X e. K /\ Y e. V /\ Z e. V ) ) -> ( ( A ` X ) x. ( Y D Z ) ) = ( ( X .x. Y ) D ( X .x. Z ) ) )