Metamath Proof Explorer

Theorem lfladdcl

Description: Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses lfladdcl.r 
|- R = ( Scalar ` W )
lfladdcl.p 
|- .+ = ( +g ` R )
lfladdcl.f 
|- F = ( LFnl ` W )
lfladdcl.w 
|- ( ph -> W e. LMod )
lfladdcl.g 
|- ( ph -> G e. F )
lfladdcl.h 
|- ( ph -> H e. F )
Assertion lfladdcl 
|- ( ph -> ( G oF .+ H ) e. F )

Proof

Step Hyp Ref Expression
1 lfladdcl.r 
 |-  R = ( Scalar ` W )
2 lfladdcl.p 
 |-  .+ = ( +g ` R )
3 lfladdcl.f 
 |-  F = ( LFnl ` W )
4 lfladdcl.w 
 |-  ( ph -> W e. LMod )
5 lfladdcl.g 
 |-  ( ph -> G e. F )
6 lfladdcl.h 
 |-  ( ph -> H e. F )
7 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> W e. LMod )
8 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> x e. ( Base ` R ) )
9 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> y e. ( Base ` R ) )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 1 10 2 lmodacl 
 |-  ( ( W e. LMod /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) e. ( Base ` R ) )
12 7 8 9 11 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x .+ y ) e. ( Base ` R ) )
13 eqid 
 |-  ( Base ` W ) = ( Base ` W )
14 1 10 13 3 lflf 
 |-  ( ( W e. LMod /\ G e. F ) -> G : ( Base ` W ) --> ( Base ` R ) )
15 4 5 14 syl2anc 
 |-  ( ph -> G : ( Base ` W ) --> ( Base ` R ) )
16 1 10 13 3 lflf 
 |-  ( ( W e. LMod /\ H e. F ) -> H : ( Base ` W ) --> ( Base ` R ) )
17 4 6 16 syl2anc 
 |-  ( ph -> H : ( Base ` W ) --> ( Base ` R ) )
18 fvexd 
 |-  ( ph -> ( Base ` W ) e. _V )
19 inidm 
 |-  ( ( Base ` W ) i^i ( Base ` W ) ) = ( Base ` W )
20 12 15 17 18 18 19 off 
 |-  ( ph -> ( G oF .+ H ) : ( Base ` W ) --> ( Base ` R ) )
21 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> W e. LMod )
22 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> x e. ( Base ` R ) )
23 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
24 eqid 
 |-  ( .s ` W ) = ( .s ` W )
25 13 1 24 10 lmodvscl 
 |-  ( ( W e. LMod /\ x e. ( Base ` R ) /\ y e. ( Base ` W ) ) -> ( x ( .s ` W ) y ) e. ( Base ` W ) )
26 21 22 23 25 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( x ( .s ` W ) y ) e. ( Base ` W ) )
27 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
28 eqid 
 |-  ( +g ` W ) = ( +g ` W )
29 13 28 lmodvacl 
 |-  ( ( W e. LMod /\ ( x ( .s ` W ) y ) e. ( Base ` W ) /\ z e. ( Base ` W ) ) -> ( ( x ( .s ` W ) y ) ( +g ` W ) z ) e. ( Base ` W ) )
30 21 26 27 29 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ( +g ` W ) z ) e. ( Base ` W ) )
31 15 ffnd 
 |-  ( ph -> G Fn ( Base ` W ) )
32 17 ffnd 
 |-  ( ph -> H Fn ( Base ` W ) )
33 eqidd 
 |-  ( ( ph /\ ( ( x ( .s ` W ) y ) ( +g ` W ) z ) e. ( Base ` W ) ) -> ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) )
34 eqidd 
 |-  ( ( ph /\ ( ( x ( .s ` W ) y ) ( +g ` W ) z ) e. ( Base ` W ) ) -> ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) )
35 31 32 18 18 19 33 34 ofval 
 |-  ( ( ph /\ ( ( x ( .s ` W ) y ) ( +g ` W ) z ) e. ( Base ` W ) ) -> ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) .+ ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
36 30 35 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) .+ ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
37 eqidd 
 |-  ( ( ph /\ y e. ( Base ` W ) ) -> ( G ` y ) = ( G ` y ) )
38 eqidd 
 |-  ( ( ph /\ y e. ( Base ` W ) ) -> ( H ` y ) = ( H ` y ) )
39 31 32 18 18 19 37 38 ofval 
 |-  ( ( ph /\ y e. ( Base ` W ) ) -> ( ( G oF .+ H ) ` y ) = ( ( G ` y ) .+ ( H ` y ) ) )
40 23 39 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G oF .+ H ) ` y ) = ( ( G ` y ) .+ ( H ` y ) ) )
41 40 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) = ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) )
42 eqidd 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( G ` z ) = ( G ` z ) )
43 eqidd 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( H ` z ) = ( H ` z ) )
44 31 32 18 18 19 42 43 ofval 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( ( G oF .+ H ) ` z ) = ( ( G ` z ) .+ ( H ` z ) ) )
45 27 44 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G oF .+ H ) ` z ) = ( ( G ` z ) .+ ( H ` z ) ) )
46 41 45 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) = ( ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) )
47 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> G e. F )
48 1 2 13 28 3 lfladd 
 |-  ( ( W e. LMod /\ G e. F /\ ( ( x ( .s ` W ) y ) e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( G ` ( x ( .s ` W ) y ) ) .+ ( G ` z ) ) )
49 21 47 26 27 48 syl112anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( G ` ( x ( .s ` W ) y ) ) .+ ( G ` z ) ) )
50 6 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> H e. F )
51 1 2 13 28 3 lfladd 
 |-  ( ( W e. LMod /\ H e. F /\ ( ( x ( .s ` W ) y ) e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( H ` ( x ( .s ` W ) y ) ) .+ ( H ` z ) ) )
52 21 50 26 27 51 syl112anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( H ` ( x ( .s ` W ) y ) ) .+ ( H ` z ) ) )
53 49 52 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) .+ ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( G ` z ) ) .+ ( ( H ` ( x ( .s ` W ) y ) ) .+ ( H ` z ) ) ) )
54 1 lmodring 
 |-  ( W e. LMod -> R e. Ring )
55 21 54 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> R e. Ring )
56 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
57 55 56 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> R e. CMnd )
58 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ ( x ( .s ` W ) y ) e. ( Base ` W ) ) -> ( G ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) )
59 21 47 26 58 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) )
60 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ z e. ( Base ` W ) ) -> ( G ` z ) e. ( Base ` R ) )
61 21 47 27 60 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` z ) e. ( Base ` R ) )
62 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ H e. F /\ ( x ( .s ` W ) y ) e. ( Base ` W ) ) -> ( H ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) )
63 21 50 26 62 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) )
64 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ H e. F /\ z e. ( Base ` W ) ) -> ( H ` z ) e. ( Base ` R ) )
65 21 50 27 64 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` z ) e. ( Base ` R ) )
66 10 2 cmn4 
 |-  ( ( R e. CMnd /\ ( ( G ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) /\ ( G ` z ) e. ( Base ` R ) ) /\ ( ( H ` ( x ( .s ` W ) y ) ) e. ( Base ` R ) /\ ( H ` z ) e. ( Base ` R ) ) ) -> ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( G ` z ) ) .+ ( ( H ` ( x ( .s ` W ) y ) ) .+ ( H ` z ) ) ) = ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( H ` ( x ( .s ` W ) y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) )
67 57 59 61 63 65 66 syl122anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( G ` z ) ) .+ ( ( H ` ( x ( .s ` W ) y ) ) .+ ( H ` z ) ) ) = ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( H ` ( x ( .s ` W ) y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) )
68 eqid 
 |-  ( .r ` R ) = ( .r ` R )
69 1 10 68 13 24 3 lflmul 
 |-  ( ( W e. LMod /\ G e. F /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) ) ) -> ( G ` ( x ( .s ` W ) y ) ) = ( x ( .r ` R ) ( G ` y ) ) )
70 21 47 22 23 69 syl112anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` ( x ( .s ` W ) y ) ) = ( x ( .r ` R ) ( G ` y ) ) )
71 1 10 68 13 24 3 lflmul 
 |-  ( ( W e. LMod /\ H e. F /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) ) ) -> ( H ` ( x ( .s ` W ) y ) ) = ( x ( .r ` R ) ( H ` y ) ) )
72 21 50 22 23 71 syl112anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` ( x ( .s ` W ) y ) ) = ( x ( .r ` R ) ( H ` y ) ) )
73 70 72 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G ` ( x ( .s ` W ) y ) ) .+ ( H ` ( x ( .s ` W ) y ) ) ) = ( ( x ( .r ` R ) ( G ` y ) ) .+ ( x ( .r ` R ) ( H ` y ) ) ) )
74 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ y e. ( Base ` W ) ) -> ( G ` y ) e. ( Base ` R ) )
75 21 47 23 74 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( G ` y ) e. ( Base ` R ) )
76 1 10 13 3 lflcl 
 |-  ( ( W e. LMod /\ H e. F /\ y e. ( Base ` W ) ) -> ( H ` y ) e. ( Base ` R ) )
77 21 50 23 76 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( H ` y ) e. ( Base ` R ) )
78 10 2 68 ringdi 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ ( G ` y ) e. ( Base ` R ) /\ ( H ` y ) e. ( Base ` R ) ) ) -> ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) = ( ( x ( .r ` R ) ( G ` y ) ) .+ ( x ( .r ` R ) ( H ` y ) ) ) )
79 55 22 75 77 78 syl13anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) = ( ( x ( .r ` R ) ( G ` y ) ) .+ ( x ( .r ` R ) ( H ` y ) ) ) )
80 73 79 eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G ` ( x ( .s ` W ) y ) ) .+ ( H ` ( x ( .s ` W ) y ) ) ) = ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) )
81 80 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( ( G ` ( x ( .s ` W ) y ) ) .+ ( H ` ( x ( .s ` W ) y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) = ( ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) )
82 53 67 81 3eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) .+ ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( ( x ( .r ` R ) ( ( G ` y ) .+ ( H ` y ) ) ) .+ ( ( G ` z ) .+ ( H ` z ) ) ) )
83 46 82 eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) = ( ( G ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) .+ ( H ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) ) )
84 36 83 eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) )
85 84 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` R ) A. y e. ( Base ` W ) A. z e. ( Base ` W ) ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) )
86 13 28 1 24 10 2 68 3 islfl 
 |-  ( W e. LMod -> ( ( G oF .+ H ) e. F <-> ( ( G oF .+ H ) : ( Base ` W ) --> ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` W ) A. z e. ( Base ` W ) ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) ) ) )
87 4 86 syl 
 |-  ( ph -> ( ( G oF .+ H ) e. F <-> ( ( G oF .+ H ) : ( Base ` W ) --> ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` W ) A. z e. ( Base ` W ) ( ( G oF .+ H ) ` ( ( x ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( x ( .r ` R ) ( ( G oF .+ H ) ` y ) ) .+ ( ( G oF .+ H ) ` z ) ) ) ) )
88 20 85 87 mpbir2and 
 |-  ( ph -> ( G oF .+ H ) e. F )