This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipsubdi

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ipsubdir.m 
|- .- = ( -g ` W )
ipsubdir.s 
|- S = ( -g ` F )
Assertion ipsubdi 
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .- C ) ) = ( ( A ., B ) S ( A ., C ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f 
 |-  F = ( Scalar ` W )
2 phllmhm.h 
 |-  ., = ( .i ` W )
3 phllmhm.v 
 |-  V = ( Base ` W )
4 ipsubdir.m 
 |-  .- = ( -g ` W )
5 ipsubdir.s 
 |-  S = ( -g ` F )
6 simpl 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. PreHil )
7 simpr1 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> A e. V )
8 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
9 8 adantr 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. LMod )
10 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
11 9 10 syl 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. Grp )
12 simpr2 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> B e. V )
13 simpr3 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> C e. V )
14 3 4 grpsubcl 
 |-  ( ( W e. Grp /\ B e. V /\ C e. V ) -> ( B .- C ) e. V )
15 11 12 13 14 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( B .- C ) e. V )
16 eqid 
 |-  ( +g ` W ) = ( +g ` W )
17 eqid 
 |-  ( +g ` F ) = ( +g ` F )
18 1 2 3 16 17 ipdi 
 |-  ( ( W e. PreHil /\ ( A e. V /\ ( B .- C ) e. V /\ C e. V ) ) -> ( A ., ( ( B .- C ) ( +g ` W ) C ) ) = ( ( A ., ( B .- C ) ) ( +g ` F ) ( A ., C ) ) )
19 6 7 15 13 18 syl13anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( ( B .- C ) ( +g ` W ) C ) ) = ( ( A ., ( B .- C ) ) ( +g ` F ) ( A ., C ) ) )
20 3 16 4 grpnpcan 
 |-  ( ( W e. Grp /\ B e. V /\ C e. V ) -> ( ( B .- C ) ( +g ` W ) C ) = B )
21 11 12 13 20 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( B .- C ) ( +g ` W ) C ) = B )
22 21 oveq2d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( ( B .- C ) ( +g ` W ) C ) ) = ( A ., B ) )
23 19 22 eqtr3d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A ., ( B .- C ) ) ( +g ` F ) ( A ., C ) ) = ( A ., B ) )
24 1 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
25 9 24 syl 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> F e. Grp )
26 eqid 
 |-  ( Base ` F ) = ( Base ` F )
27 1 2 3 26 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. ( Base ` F ) )
28 6 7 12 27 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., B ) e. ( Base ` F ) )
29 1 2 3 26 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` F ) )
30 6 7 13 29 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., C ) e. ( Base ` F ) )
31 1 2 3 26 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ ( B .- C ) e. V ) -> ( A ., ( B .- C ) ) e. ( Base ` F ) )
32 6 7 15 31 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .- C ) ) e. ( Base ` F ) )
33 26 17 5 grpsubadd 
 |-  ( ( F e. Grp /\ ( ( A ., B ) e. ( Base ` F ) /\ ( A ., C ) e. ( Base ` F ) /\ ( A ., ( B .- C ) ) e. ( Base ` F ) ) ) -> ( ( ( A ., B ) S ( A ., C ) ) = ( A ., ( B .- C ) ) <-> ( ( A ., ( B .- C ) ) ( +g ` F ) ( A ., C ) ) = ( A ., B ) ) )
34 25 28 30 32 33 syl13anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( A ., B ) S ( A ., C ) ) = ( A ., ( B .- C ) ) <-> ( ( A ., ( B .- C ) ) ( +g ` F ) ( A ., C ) ) = ( A ., B ) ) )
35 23 34 mpbird 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A ., B ) S ( A ., C ) ) = ( A ., ( B .- C ) ) )
36 35 eqcomd 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .- C ) ) = ( ( A ., B ) S ( A ., C ) ) )