Metamath Proof Explorer

Theorem lfladdcl

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

Ref Expression
Hypotheses lfladdcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
lfladdcl.p ⊢ + = ( +g ‘ 𝑅 )
lfladdcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfladdcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lfladdcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lfladdcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion lfladdcl ( 𝜑 → ( 𝐺 ∘f + 𝐻 ) ∈ 𝐹 )

Proof

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