Metamath Proof Explorer

Theorem lflmul

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

Ref Expression
Hypotheses lflmul.d 
|- D = ( Scalar ` W )
lflmul.k 
|- K = ( Base ` D )
lflmul.t 
|- .X. = ( .r ` D )
lflmul.v 
|- V = ( Base ` W )
lflmul.s 
|- .x. = ( .s ` W )
lflmul.f 
|- F = ( LFnl ` W )
Assertion lflmul 
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( R .x. X ) ) = ( R .X. ( G ` X ) ) )

Proof

Step Hyp Ref Expression
1 lflmul.d 
 |-  D = ( Scalar ` W )
2 lflmul.k 
 |-  K = ( Base ` D )
3 lflmul.t 
 |-  .X. = ( .r ` D )
4 lflmul.v 
 |-  V = ( Base ` W )
5 lflmul.s 
 |-  .x. = ( .s ` W )
6 lflmul.f 
 |-  F = ( LFnl ` W )
7 simp1 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> W e. LMod )
8 simp2 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> G e. F )
9 simp3l 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> R e. K )
10 simp3r 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> X e. V )
11 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
12 4 11 lmod0vcl 
 |-  ( W e. LMod -> ( 0g ` W ) e. V )
13 12 3ad2ant1 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( 0g ` W ) e. V )
14 eqid 
 |-  ( +g ` W ) = ( +g ` W )
15 eqid 
 |-  ( +g ` D ) = ( +g ` D )
16 4 14 1 5 2 15 3 6 lfli 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V /\ ( 0g ` W ) e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) )
17 7 8 9 10 13 16 syl113anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) )
18 4 1 5 2 lmodvscl 
 |-  ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )
19 7 9 10 18 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( R .x. X ) e. V )
20 4 14 11 lmod0vrid 
 |-  ( ( W e. LMod /\ ( R .x. X ) e. V ) -> ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( R .x. X ) )
21 7 19 20 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( R .x. X ) )
22 21 fveq2d 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( G ` ( R .x. X ) ) )
23 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
24 1 23 11 6 lfl0 
 |-  ( ( W e. LMod /\ G e. F ) -> ( G ` ( 0g ` W ) ) = ( 0g ` D ) )
25 24 3adant3 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( 0g ` W ) ) = ( 0g ` D ) )
26 25 oveq2d 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) )
27 1 lmodfgrp 
 |-  ( W e. LMod -> D e. Grp )
28 27 3ad2ant1 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> D e. Grp )
29 1 2 4 6 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ X e. V ) -> ( G ` X ) e. K )
30 29 3adant3l 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` X ) e. K )
31 1 2 3 lmodmcl 
 |-  ( ( W e. LMod /\ R e. K /\ ( G ` X ) e. K ) -> ( R .X. ( G ` X ) ) e. K )
32 7 9 30 31 syl3anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( R .X. ( G ` X ) ) e. K )
33 2 15 23 grprid 
 |-  ( ( D e. Grp /\ ( R .X. ( G ` X ) ) e. K ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) = ( R .X. ( G ` X ) ) )
34 28 32 33 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) = ( R .X. ( G ` X ) ) )
35 26 34 eqtrd 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) = ( R .X. ( G ` X ) ) )
36 17 22 35 3eqtr3d 
 |-  ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( R .x. X ) ) = ( R .X. ( G ` X ) ) )