Step | Hyp | Ref
| Expression |
1 | | lfladdcl.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑊 ∈ LMod) |
3 | | simprl 790 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑥 ∈ (Base‘𝑅)) |
4 | | simprr 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → 𝑦 ∈ (Base‘𝑅)) |
5 | | lfladdcl.r |
. . . . 5
⊢ 𝑅 = (Scalar‘𝑊) |
6 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
7 | | lfladdcl.p |
. . . . 5
⊢ + =
(+g‘𝑅) |
8 | 5, 6, 7 | lmodacl 18697 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥 + 𝑦) ∈ (Base‘𝑅)) |
9 | 2, 3, 4, 8 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))) → (𝑥 + 𝑦) ∈ (Base‘𝑅)) |
10 | | lfladdcl.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
11 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
12 | | lfladdcl.f |
. . . . 5
⊢ 𝐹 = (LFnl‘𝑊) |
13 | 5, 6, 11, 12 | lflf 33368 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝐺:(Base‘𝑊)⟶(Base‘𝑅)) |
14 | 1, 10, 13 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝐺:(Base‘𝑊)⟶(Base‘𝑅)) |
15 | | lfladdcl.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐹) |
16 | 5, 6, 11, 12 | lflf 33368 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹) → 𝐻:(Base‘𝑊)⟶(Base‘𝑅)) |
17 | 1, 15, 16 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝐻:(Base‘𝑊)⟶(Base‘𝑅)) |
18 | | fvex 6113 |
. . . 4
⊢
(Base‘𝑊)
∈ V |
19 | 18 | a1i 11 |
. . 3
⊢ (𝜑 → (Base‘𝑊) ∈ V) |
20 | | inidm 3784 |
. . 3
⊢
((Base‘𝑊)
∩ (Base‘𝑊)) =
(Base‘𝑊) |
21 | 9, 14, 17, 19, 19, 20 | off 6810 |
. 2
⊢ (𝜑 → (𝐺 ∘𝑓 + 𝐻):(Base‘𝑊)⟶(Base‘𝑅)) |
22 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑊 ∈ LMod) |
23 | | simpr1 1060 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑅)) |
24 | | simpr2 1061 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊)) |
25 | | eqid 2610 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
26 | 11, 5, 25, 6 | lmodvscl 18703 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊)) |
27 | 22, 23, 24, 26 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊)) |
28 | | simpr3 1062 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊)) |
29 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
30 | 11, 29 | lmodvacl 18700 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑥(
·𝑠 ‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊)) → ((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ (Base‘𝑊)) |
31 | 22, 27, 28, 30 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ (Base‘𝑊)) |
32 | | ffn 5958 |
. . . . . . 7
⊢ (𝐺:(Base‘𝑊)⟶(Base‘𝑅) → 𝐺 Fn (Base‘𝑊)) |
33 | 14, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn (Base‘𝑊)) |
34 | | ffn 5958 |
. . . . . . 7
⊢ (𝐻:(Base‘𝑊)⟶(Base‘𝑅) → 𝐻 Fn (Base‘𝑊)) |
35 | 17, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 Fn (Base‘𝑊)) |
36 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ (Base‘𝑊)) → (𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) |
37 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ (Base‘𝑊)) → (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) |
38 | 33, 35, 19, 19, 20, 36, 37 | ofval 6804 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ (Base‘𝑊)) → ((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) + (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
39 | 31, 38 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) + (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
40 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝐺‘𝑦) = (𝐺‘𝑦)) |
41 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝐻‘𝑦) = (𝐻‘𝑦)) |
42 | 33, 35, 19, 19, 20, 40, 41 | ofval 6804 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝐺 ∘𝑓 + 𝐻)‘𝑦) = ((𝐺‘𝑦) + (𝐻‘𝑦))) |
43 | 24, 42 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺 ∘𝑓 + 𝐻)‘𝑦) = ((𝐺‘𝑦) + (𝐻‘𝑦))) |
44 | 43 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) = (𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦)))) |
45 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
46 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝐻‘𝑧) = (𝐻‘𝑧)) |
47 | 33, 35, 19, 19, 20, 45, 46 | ofval 6804 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝑊)) → ((𝐺 ∘𝑓 + 𝐻)‘𝑧) = ((𝐺‘𝑧) + (𝐻‘𝑧))) |
48 | 28, 47 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺 ∘𝑓 + 𝐻)‘𝑧) = ((𝐺‘𝑧) + (𝐻‘𝑧))) |
49 | 44, 48 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧)) = ((𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧)))) |
50 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝐺 ∈ 𝐹) |
51 | 5, 7, 11, 29, 12 | lfladd 33371 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐺‘𝑧))) |
52 | 22, 50, 27, 28, 51 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐺‘𝑧))) |
53 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝐻 ∈ 𝐹) |
54 | 5, 7, 11, 29, 12 | lfladd 33371 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘𝑧))) |
55 | 22, 53, 27, 28, 54 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘𝑧))) |
56 | 52, 55 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) + (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐺‘𝑧)) + ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘𝑧)))) |
57 | 5 | lmodring 18694 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Ring) |
58 | 22, 57 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑅 ∈ Ring) |
59 | | ringcmn 18404 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
60 | 58, 59 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → 𝑅 ∈ CMnd) |
61 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊)) → (𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅)) |
62 | 22, 50, 27, 61 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅)) |
63 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
64 | 22, 50, 28, 63 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
65 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥( ·𝑠
‘𝑊)𝑦) ∈ (Base‘𝑊)) → (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅)) |
66 | 22, 53, 27, 65 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅)) |
67 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ 𝑧 ∈ (Base‘𝑊)) → (𝐻‘𝑧) ∈ (Base‘𝑅)) |
68 | 22, 53, 28, 67 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘𝑧) ∈ (Base‘𝑅)) |
69 | 6, 7 | cmn4 18035 |
. . . . . . 7
⊢ ((𝑅 ∈ CMnd ∧ ((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅) ∧ (𝐺‘𝑧) ∈ (Base‘𝑅)) ∧ ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) ∈ (Base‘𝑅) ∧ (𝐻‘𝑧) ∈ (Base‘𝑅))) → (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐺‘𝑧)) + ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘𝑧))) = (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧)))) |
70 | 60, 62, 64, 66, 68, 69 | syl122anc 1327 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐺‘𝑧)) + ((𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘𝑧))) = (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧)))) |
71 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
72 | 5, 6, 71, 11, 25, 12 | lflmul 33373 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (𝑥(.r‘𝑅)(𝐺‘𝑦))) |
73 | 22, 50, 23, 24, 72 | syl112anc 1322 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (𝑥(.r‘𝑅)(𝐺‘𝑦))) |
74 | 5, 6, 71, 11, 25, 12 | lflmul 33373 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (𝑥(.r‘𝑅)(𝐻‘𝑦))) |
75 | 22, 53, 23, 24, 74 | syl112anc 1322 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦)) = (𝑥(.r‘𝑅)(𝐻‘𝑦))) |
76 | 73, 75 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦))) = ((𝑥(.r‘𝑅)(𝐺‘𝑦)) + (𝑥(.r‘𝑅)(𝐻‘𝑦)))) |
77 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝐺‘𝑦) ∈ (Base‘𝑅)) |
78 | 22, 50, 24, 77 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐺‘𝑦) ∈ (Base‘𝑅)) |
79 | 5, 6, 11, 12 | lflcl 33369 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ 𝑦 ∈ (Base‘𝑊)) → (𝐻‘𝑦) ∈ (Base‘𝑅)) |
80 | 22, 53, 24, 79 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝐻‘𝑦) ∈ (Base‘𝑅)) |
81 | 6, 7, 71 | ringdi 18389 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ (𝐺‘𝑦) ∈ (Base‘𝑅) ∧ (𝐻‘𝑦) ∈ (Base‘𝑅))) → (𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦))) = ((𝑥(.r‘𝑅)(𝐺‘𝑦)) + (𝑥(.r‘𝑅)(𝐻‘𝑦)))) |
82 | 58, 23, 78, 80, 81 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦))) = ((𝑥(.r‘𝑅)(𝐺‘𝑦)) + (𝑥(.r‘𝑅)(𝐻‘𝑦)))) |
83 | 76, 82 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦))) = (𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦)))) |
84 | 83 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → (((𝐺‘(𝑥( ·𝑠
‘𝑊)𝑦)) + (𝐻‘(𝑥( ·𝑠
‘𝑊)𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧))) = ((𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧)))) |
85 | 56, 70, 84 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) + (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧))) = ((𝑥(.r‘𝑅)((𝐺‘𝑦) + (𝐻‘𝑦))) + ((𝐺‘𝑧) + (𝐻‘𝑧)))) |
86 | 49, 85 | eqtr4d 2647 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧)) = ((𝐺‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) + (𝐻‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)))) |
87 | 39, 86 | eqtr4d 2647 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊))) → ((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧))) |
88 | 87 | ralrimivvva 2955 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑊)∀𝑧 ∈ (Base‘𝑊)((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧))) |
89 | 11, 29, 5, 25, 6, 7,
71, 12 | islfl 33365 |
. . 3
⊢ (𝑊 ∈ LMod → ((𝐺 ∘𝑓
+ 𝐻) ∈ 𝐹 ↔ ((𝐺 ∘𝑓 + 𝐻):(Base‘𝑊)⟶(Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑊)∀𝑧 ∈ (Base‘𝑊)((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧))))) |
90 | 1, 89 | syl 17 |
. 2
⊢ (𝜑 → ((𝐺 ∘𝑓 + 𝐻) ∈ 𝐹 ↔ ((𝐺 ∘𝑓 + 𝐻):(Base‘𝑊)⟶(Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑊)∀𝑧 ∈ (Base‘𝑊)((𝐺 ∘𝑓 + 𝐻)‘((𝑥( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)) = ((𝑥(.r‘𝑅)((𝐺 ∘𝑓 + 𝐻)‘𝑦)) + ((𝐺 ∘𝑓 + 𝐻)‘𝑧))))) |
91 | 21, 88, 90 | mpbir2and 959 |
1
⊢ (𝜑 → (𝐺 ∘𝑓 + 𝐻) ∈ 𝐹) |