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 ) ) )