Metamath Proof Explorer

Theorem lmodsubdir

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr2 analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lmodsubdir.v 
|- V = ( Base ` W )
lmodsubdir.t 
|- .x. = ( .s ` W )
lmodsubdir.f 
|- F = ( Scalar ` W )
lmodsubdir.k 
|- K = ( Base ` F )
lmodsubdir.m 
|- .- = ( -g ` W )
lmodsubdir.s 
|- S = ( -g ` F )
lmodsubdir.w 
|- ( ph -> W e. LMod )
lmodsubdir.a 
|- ( ph -> A e. K )
lmodsubdir.b 
|- ( ph -> B e. K )
lmodsubdir.x 
|- ( ph -> X e. V )
Assertion lmodsubdir 
|- ( ph -> ( ( A S B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )

Proof

Step Hyp Ref Expression
1 lmodsubdir.v 
 |-  V = ( Base ` W )
2 lmodsubdir.t 
 |-  .x. = ( .s ` W )
3 lmodsubdir.f 
 |-  F = ( Scalar ` W )
4 lmodsubdir.k 
 |-  K = ( Base ` F )
5 lmodsubdir.m 
 |-  .- = ( -g ` W )
6 lmodsubdir.s 
 |-  S = ( -g ` F )
7 lmodsubdir.w 
 |-  ( ph -> W e. LMod )
8 lmodsubdir.a 
 |-  ( ph -> A e. K )
9 lmodsubdir.b 
 |-  ( ph -> B e. K )
10 lmodsubdir.x 
 |-  ( ph -> X e. V )
11 3 lmodring 
 |-  ( W e. LMod -> F e. Ring )
12 7 11 syl 
 |-  ( ph -> F e. Ring )
13 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
14 12 13 syl 
 |-  ( ph -> F e. Grp )
15 eqid 
 |-  ( invg ` F ) = ( invg ` F )
16 4 15 grpinvcl 
 |-  ( ( F e. Grp /\ B e. K ) -> ( ( invg ` F ) ` B ) e. K )
17 14 9 16 syl2anc 
 |-  ( ph -> ( ( invg ` F ) ` B ) e. K )
18 eqid 
 |-  ( +g ` W ) = ( +g ` W )
19 eqid 
 |-  ( +g ` F ) = ( +g ` F )
20 1 18 3 2 4 19 lmodvsdir 
 |-  ( ( W e. LMod /\ ( A e. K /\ ( ( invg ` F ) ` B ) e. K /\ X e. V ) ) -> ( ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) .x. X ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` B ) .x. X ) ) )
21 7 8 17 10 20 syl13anc 
 |-  ( ph -> ( ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) .x. X ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` B ) .x. X ) ) )
22 eqid 
 |-  ( .r ` F ) = ( .r ` F )
23 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
24 4 22 23 15 12 9 ringnegl 
 |-  ( ph -> ( ( ( invg ` F ) ` ( 1r ` F ) ) ( .r ` F ) B ) = ( ( invg ` F ) ` B ) )
25 24 oveq1d 
 |-  ( ph -> ( ( ( ( invg ` F ) ` ( 1r ` F ) ) ( .r ` F ) B ) .x. X ) = ( ( ( invg ` F ) ` B ) .x. X ) )
26 4 23 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. K )
27 12 26 syl 
 |-  ( ph -> ( 1r ` F ) e. K )
28 4 15 grpinvcl 
 |-  ( ( F e. Grp /\ ( 1r ` F ) e. K ) -> ( ( invg ` F ) ` ( 1r ` F ) ) e. K )
29 14 27 28 syl2anc 
 |-  ( ph -> ( ( invg ` F ) ` ( 1r ` F ) ) e. K )
30 1 3 2 4 22 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( ( invg ` F ) ` ( 1r ` F ) ) e. K /\ B e. K /\ X e. V ) ) -> ( ( ( ( invg ` F ) ` ( 1r ` F ) ) ( .r ` F ) B ) .x. X ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) )
31 7 29 9 10 30 syl13anc 
 |-  ( ph -> ( ( ( ( invg ` F ) ` ( 1r ` F ) ) ( .r ` F ) B ) .x. X ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) )
32 25 31 eqtr3d 
 |-  ( ph -> ( ( ( invg ` F ) ` B ) .x. X ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) )
33 32 oveq2d 
 |-  ( ph -> ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` B ) .x. X ) ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) ) )
34 21 33 eqtrd 
 |-  ( ph -> ( ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) .x. X ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) ) )
35 4 19 15 6 grpsubval 
 |-  ( ( A e. K /\ B e. K ) -> ( A S B ) = ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) )
36 8 9 35 syl2anc 
 |-  ( ph -> ( A S B ) = ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) )
37 36 oveq1d 
 |-  ( ph -> ( ( A S B ) .x. X ) = ( ( A ( +g ` F ) ( ( invg ` F ) ` B ) ) .x. X ) )
38 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ X e. V ) -> ( A .x. X ) e. V )
39 7 8 10 38 syl3anc 
 |-  ( ph -> ( A .x. X ) e. V )
40 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ B e. K /\ X e. V ) -> ( B .x. X ) e. V )
41 7 9 10 40 syl3anc 
 |-  ( ph -> ( B .x. X ) e. V )
42 1 18 5 3 2 15 23 lmodvsubval2 
 |-  ( ( W e. LMod /\ ( A .x. X ) e. V /\ ( B .x. X ) e. V ) -> ( ( A .x. X ) .- ( B .x. X ) ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) ) )
43 7 39 41 42 syl3anc 
 |-  ( ph -> ( ( A .x. X ) .- ( B .x. X ) ) = ( ( A .x. X ) ( +g ` W ) ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. ( B .x. X ) ) ) )
44 34 37 43 3eqtr4d 
 |-  ( ph -> ( ( A S B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )