Metamath Proof Explorer

Theorem lmodsubdi

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr1 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014)

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

Proof

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