Metamath Proof Explorer

Theorem lflsub

Description: Property of a linear functional. ( lnfnaddi analog.) (Contributed by NM, 18-Apr-2014)

Ref Expression
Hypotheses lflsub.d 
|- D = ( Scalar ` W )
lflsub.m 
|- M = ( -g ` D )
lflsub.v 
|- V = ( Base ` W )
lflsub.a 
|- .- = ( -g ` W )
lflsub.f 
|- F = ( LFnl ` W )
Assertion lflsub 
|- ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .- Y ) ) = ( ( G ` X ) M ( G ` Y ) ) )

Proof

Step Hyp Ref Expression
1 lflsub.d 
 |-  D = ( Scalar ` W )
2 lflsub.m 
 |-  M = ( -g ` D )
3 lflsub.v 
 |-  V = ( Base ` W )
4 lflsub.a 
 |-  .- = ( -g ` W )
5 lflsub.f 
 |-  F = ( LFnl ` W )
6 simp1 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> W e. LMod )
7 simp3l 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> X e. V )
8 1 lmodring 
 |-  ( W e. LMod -> D e. Ring )
9 8 3ad2ant1 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> D e. Ring )
10 ringgrp 
 |-  ( D e. Ring -> D e. Grp )
11 9 10 syl 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> D e. Grp )
12 eqid 
 |-  ( Base ` D ) = ( Base ` D )
13 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
14 12 13 ringidcl 
 |-  ( D e. Ring -> ( 1r ` D ) e. ( Base ` D ) )
15 9 14 syl 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( 1r ` D ) e. ( Base ` D ) )
16 eqid 
 |-  ( invg ` D ) = ( invg ` D )
17 12 16 grpinvcl 
 |-  ( ( D e. Grp /\ ( 1r ` D ) e. ( Base ` D ) ) -> ( ( invg ` D ) ` ( 1r ` D ) ) e. ( Base ` D ) )
18 11 15 17 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( invg ` D ) ` ( 1r ` D ) ) e. ( Base ` D ) )
19 simp3r 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
20 eqid 
 |-  ( .s ` W ) = ( .s ` W )
21 3 1 20 12 lmodvscl 
 |-  ( ( W e. LMod /\ ( ( invg ` D ) ` ( 1r ` D ) ) e. ( Base ` D ) /\ Y e. V ) -> ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) e. V )
22 6 18 19 21 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) e. V )
23 eqid 
 |-  ( +g ` W ) = ( +g ` W )
24 3 23 lmodcom 
 |-  ( ( W e. LMod /\ X e. V /\ ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) e. V ) -> ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) = ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ( +g ` W ) X ) )
25 6 7 22 24 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) = ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ( +g ` W ) X ) )
26 25 fveq2d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) ) = ( G ` ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ( +g ` W ) X ) ) )
27 simp2 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> G e. F )
28 eqid 
 |-  ( +g ` D ) = ( +g ` D )
29 eqid 
 |-  ( .r ` D ) = ( .r ` D )
30 3 23 1 20 12 28 29 5 lfli 
 |-  ( ( W e. LMod /\ G e. F /\ ( ( ( invg ` D ) ` ( 1r ` D ) ) e. ( Base ` D ) /\ Y e. V /\ X e. V ) ) -> ( G ` ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ( +g ` W ) X ) ) = ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .r ` D ) ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) )
31 6 27 18 19 7 30 syl113anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ( +g ` W ) X ) ) = ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .r ` D ) ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) )
32 1 12 3 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ Y e. V ) -> ( G ` Y ) e. ( Base ` D ) )
33 32 3adant3l 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` Y ) e. ( Base ` D ) )
34 12 29 13 16 9 33 ringnegl 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .r ` D ) ( G ` Y ) ) = ( ( invg ` D ) ` ( G ` Y ) ) )
35 34 oveq1d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .r ` D ) ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) = ( ( ( invg ` D ) ` ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) )
36 ringabl 
 |-  ( D e. Ring -> D e. Abel )
37 9 36 syl 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> D e. Abel )
38 12 16 grpinvcl 
 |-  ( ( D e. Grp /\ ( G ` Y ) e. ( Base ` D ) ) -> ( ( invg ` D ) ` ( G ` Y ) ) e. ( Base ` D ) )
39 11 33 38 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( invg ` D ) ` ( G ` Y ) ) e. ( Base ` D ) )
40 1 12 3 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` D ) )
41 40 3adant3r 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` X ) e. ( Base ` D ) )
42 12 28 ablcom 
 |-  ( ( D e. Abel /\ ( ( invg ` D ) ` ( G ` Y ) ) e. ( Base ` D ) /\ ( G ` X ) e. ( Base ` D ) ) -> ( ( ( invg ` D ) ` ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
43 37 39 41 42 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( invg ` D ) ` ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
44 35 43 eqtrd 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .r ` D ) ( G ` Y ) ) ( +g ` D ) ( G ` X ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
45 26 31 44 3eqtrd 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
46 3 23 4 1 20 16 13 lmodvsubval2 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) = ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) )
47 6 7 19 46 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( X .- Y ) = ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) )
48 47 fveq2d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .- Y ) ) = ( G ` ( X ( +g ` W ) ( ( ( invg ` D ) ` ( 1r ` D ) ) ( .s ` W ) Y ) ) ) )
49 12 28 16 2 grpsubval 
 |-  ( ( ( G ` X ) e. ( Base ` D ) /\ ( G ` Y ) e. ( Base ` D ) ) -> ( ( G ` X ) M ( G ` Y ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
50 41 33 49 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( G ` X ) M ( G ` Y ) ) = ( ( G ` X ) ( +g ` D ) ( ( invg ` D ) ` ( G ` Y ) ) ) )
51 45 48 50 3eqtr4d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .- Y ) ) = ( ( G ` X ) M ( G ` Y ) ) )