# Metamath Proof Explorer

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

Ref Expression
Hypotheses lfladdcl.r $⊢ R = Scalar ⁡ W$
lfladdcl.f $⊢ F = LFnl ⁡ W$
lfladdcl.w $⊢ φ → W ∈ LMod$
lfladdcl.g $⊢ φ → G ∈ F$
lfladdcl.h $⊢ φ → H ∈ F$

### Proof

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