Metamath Proof Explorer

Theorem lmodsubvs

Description: Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 lmodsubvs.v 
 |-  V = ( Base ` W )
2 lmodsubvs.p 
 |-  .+ = ( +g ` W )
3 lmodsubvs.m 
 |-  .- = ( -g ` W )
4 lmodsubvs.t 
 |-  .x. = ( .s ` W )
5 lmodsubvs.f 
 |-  F = ( Scalar ` W )
6 lmodsubvs.k 
 |-  K = ( Base ` F )
7 lmodsubvs.n 
 |-  N = ( invg ` F )
8 lmodsubvs.w 
 |-  ( ph -> W e. LMod )
9 lmodsubvs.a 
 |-  ( ph -> A e. K )
10 lmodsubvs.x 
 |-  ( ph -> X e. V )
11 lmodsubvs.y 
 |-  ( ph -> Y e. V )
12 1 5 4 6 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ Y e. V ) -> ( A .x. Y ) e. V )
13 8 9 11 12 syl3anc 
 |-  ( ph -> ( A .x. Y ) e. V )
14 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
15 1 2 3 5 4 7 14 lmodvsubval2 
 |-  ( ( W e. LMod /\ X e. V /\ ( A .x. Y ) e. V ) -> ( X .- ( A .x. Y ) ) = ( X .+ ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) ) )
16 8 10 13 15 syl3anc 
 |-  ( ph -> ( X .- ( A .x. Y ) ) = ( X .+ ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) ) )
17 5 lmodring 
 |-  ( W e. LMod -> F e. Ring )
18 8 17 syl 
 |-  ( ph -> F e. Ring )
19 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
20 18 19 syl 
 |-  ( ph -> F e. Grp )
21 6 14 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. K )
22 18 21 syl 
 |-  ( ph -> ( 1r ` F ) e. K )
23 6 7 grpinvcl 
 |-  ( ( F e. Grp /\ ( 1r ` F ) e. K ) -> ( N ` ( 1r ` F ) ) e. K )
24 20 22 23 syl2anc 
 |-  ( ph -> ( N ` ( 1r ` F ) ) e. K )
25 eqid 
 |-  ( .r ` F ) = ( .r ` F )
26 1 5 4 6 25 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( N ` ( 1r ` F ) ) e. K /\ A e. K /\ Y e. V ) ) -> ( ( ( N ` ( 1r ` F ) ) ( .r ` F ) A ) .x. Y ) = ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) )
27 8 24 9 11 26 syl13anc 
 |-  ( ph -> ( ( ( N ` ( 1r ` F ) ) ( .r ` F ) A ) .x. Y ) = ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) )
28 6 25 14 7 18 9 ringnegl 
 |-  ( ph -> ( ( N ` ( 1r ` F ) ) ( .r ` F ) A ) = ( N ` A ) )
29 28 oveq1d 
 |-  ( ph -> ( ( ( N ` ( 1r ` F ) ) ( .r ` F ) A ) .x. Y ) = ( ( N ` A ) .x. Y ) )
30 27 29 eqtr3d 
 |-  ( ph -> ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) = ( ( N ` A ) .x. Y ) )
31 30 oveq2d 
 |-  ( ph -> ( X .+ ( ( N ` ( 1r ` F ) ) .x. ( A .x. Y ) ) ) = ( X .+ ( ( N ` A ) .x. Y ) ) )
32 16 31 eqtrd 
 |-  ( ph -> ( X .- ( A .x. Y ) ) = ( X .+ ( ( N ` A ) .x. Y ) ) )