Metamath Proof Explorer

Theorem lfladd

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

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

Proof

Step Hyp Ref Expression
1 lfladd.d 
 |-  D = ( Scalar ` W )
2 lfladd.p 
 |-  .+^ = ( +g ` D )
3 lfladd.v 
 |-  V = ( Base ` W )
4 lfladd.a 
 |-  .+ = ( +g ` W )
5 lfladd.f 
 |-  F = ( LFnl ` W )
6 simp1 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> W e. LMod )
7 simp2 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> G e. F )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
10 1 8 9 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` D ) e. ( Base ` D ) )
11 10 3ad2ant1 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( 1r ` D ) e. ( Base ` D ) )
12 simp3l 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> X e. V )
13 simp3r 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> Y e. V )
14 eqid 
 |-  ( .s ` W ) = ( .s ` W )
15 eqid 
 |-  ( .r ` D ) = ( .r ` D )
16 3 4 1 14 8 2 15 5 lfli 
 |-  ( ( W e. LMod /\ G e. F /\ ( ( 1r ` D ) e. ( Base ` D ) /\ X e. V /\ Y e. V ) ) -> ( G ` ( ( ( 1r ` D ) ( .s ` W ) X ) .+ Y ) ) = ( ( ( 1r ` D ) ( .r ` D ) ( G ` X ) ) .+^ ( G ` Y ) ) )
17 6 7 11 12 13 16 syl113anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( ( ( 1r ` D ) ( .s ` W ) X ) .+ Y ) ) = ( ( ( 1r ` D ) ( .r ` D ) ( G ` X ) ) .+^ ( G ` Y ) ) )
18 3 1 14 9 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` D ) ( .s ` W ) X ) = X )
19 6 12 18 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( 1r ` D ) ( .s ` W ) X ) = X )
20 19 fvoveq1d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( ( ( 1r ` D ) ( .s ` W ) X ) .+ Y ) ) = ( G ` ( X .+ Y ) ) )
21 1 lmodring 
 |-  ( W e. LMod -> D e. Ring )
22 21 3ad2ant1 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> D e. Ring )
23 1 8 3 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` D ) )
24 23 3adant3r 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` X ) e. ( Base ` D ) )
25 8 15 9 ringlidm 
 |-  ( ( D e. Ring /\ ( G ` X ) e. ( Base ` D ) ) -> ( ( 1r ` D ) ( .r ` D ) ( G ` X ) ) = ( G ` X ) )
26 22 24 25 syl2anc 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( 1r ` D ) ( .r ` D ) ( G ` X ) ) = ( G ` X ) )
27 26 oveq1d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( ( ( 1r ` D ) ( .r ` D ) ( G ` X ) ) .+^ ( G ` Y ) ) = ( ( G ` X ) .+^ ( G ` Y ) ) )
28 17 20 27 3eqtr3d 
 |-  ( ( W e. LMod /\ G e. F /\ ( X e. V /\ Y e. V ) ) -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) .+^ ( G ` Y ) ) )