Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2610 |
. 2
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
3 | | eqid 2610 |
. 2
⊢ (
·𝑠 ‘𝑁) = ( ·𝑠
‘𝑁) |
4 | | eqid 2610 |
. 2
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
5 | | eqid 2610 |
. 2
⊢
(Scalar‘𝑁) =
(Scalar‘𝑁) |
6 | | eqid 2610 |
. 2
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
7 | | lmhmlmod1 18854 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑀 ∈ LMod) |
8 | 7 | adantr 480 |
. 2
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑀 ∈ LMod) |
9 | | lmhmlmod2 18853 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝑁 ∈ LMod) |
10 | 9 | adantr 480 |
. 2
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑁 ∈ LMod) |
11 | 4, 5 | lmhmsca 18851 |
. . 3
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → (Scalar‘𝑁) = (Scalar‘𝑀)) |
12 | 11 | adantr 480 |
. 2
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (Scalar‘𝑁) = (Scalar‘𝑀)) |
13 | | lmodabl 18733 |
. . . 4
⊢ (𝑁 ∈ LMod → 𝑁 ∈ Abel) |
14 | 10, 13 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑁 ∈ Abel) |
15 | | lmghm 18852 |
. . . 4
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
16 | 15 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐹 ∈ (𝑀 GrpHom 𝑁)) |
17 | | lmghm 18852 |
. . . 4
⊢ (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺 ∈ (𝑀 GrpHom 𝑁)) |
18 | 17 | adantl 481 |
. . 3
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐺 ∈ (𝑀 GrpHom 𝑁)) |
19 | | lmhmplusg.p |
. . . 4
⊢ + =
(+g‘𝑁) |
20 | 19 | ghmplusg 18072 |
. . 3
⊢ ((𝑁 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpHom 𝑁) ∧ 𝐺 ∈ (𝑀 GrpHom 𝑁)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑀 GrpHom 𝑁)) |
21 | 14, 16, 18, 20 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑀 GrpHom 𝑁)) |
22 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐹 ∈ (𝑀 LMHom 𝑁)) |
23 | | simprl 790 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘(Scalar‘𝑀))) |
24 | | simprr 792 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑦 ∈ (Base‘𝑀)) |
25 | 4, 6, 1, 2, 3 | lmhmlin 18856 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥( ·𝑠
‘𝑁)(𝐹‘𝑦))) |
26 | 22, 23, 24, 25 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥( ·𝑠
‘𝑁)(𝐹‘𝑦))) |
27 | | simplr 788 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐺 ∈ (𝑀 LMHom 𝑁)) |
28 | 4, 6, 1, 2, 3 | lmhmlin 18856 |
. . . . . 6
⊢ ((𝐺 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥( ·𝑠
‘𝑁)(𝐺‘𝑦))) |
29 | 27, 23, 24, 28 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥( ·𝑠
‘𝑁)(𝐺‘𝑦))) |
30 | 26, 29 | oveq12d 6567 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) + (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦))) = ((𝑥( ·𝑠
‘𝑁)(𝐹‘𝑦)) + (𝑥( ·𝑠
‘𝑁)(𝐺‘𝑦)))) |
31 | 9 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑁 ∈ LMod) |
32 | 11 | fveq2d 6107 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → (Base‘(Scalar‘𝑁)) =
(Base‘(Scalar‘𝑀))) |
33 | 32 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (Base‘(Scalar‘𝑁)) =
(Base‘(Scalar‘𝑀))) |
34 | 23, 33 | eleqtrrd 2691 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘(Scalar‘𝑁))) |
35 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑁) =
(Base‘𝑁) |
36 | 1, 35 | lmhmf 18855 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑀 LMHom 𝑁) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
37 | 36 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
38 | 37, 24 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘𝑦) ∈ (Base‘𝑁)) |
39 | 1, 35 | lmhmf 18855 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁)) |
40 | 39 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁)) |
41 | 40, 24 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺‘𝑦) ∈ (Base‘𝑁)) |
42 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑁)) |
43 | 35, 19, 5, 3, 42 | lmodvsdi 18709 |
. . . . 5
⊢ ((𝑁 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑁)) ∧ (𝐹‘𝑦) ∈ (Base‘𝑁) ∧ (𝐺‘𝑦) ∈ (Base‘𝑁))) → (𝑥( ·𝑠
‘𝑁)((𝐹‘𝑦) + (𝐺‘𝑦))) = ((𝑥( ·𝑠
‘𝑁)(𝐹‘𝑦)) + (𝑥( ·𝑠
‘𝑁)(𝐺‘𝑦)))) |
44 | 31, 34, 38, 41, 43 | syl13anc 1320 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠
‘𝑁)((𝐹‘𝑦) + (𝐺‘𝑦))) = ((𝑥( ·𝑠
‘𝑁)(𝐹‘𝑦)) + (𝑥( ·𝑠
‘𝑁)(𝐺‘𝑦)))) |
45 | 30, 44 | eqtr4d 2647 |
. . 3
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) + (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦))) = (𝑥( ·𝑠
‘𝑁)((𝐹‘𝑦) + (𝐺‘𝑦)))) |
46 | | ffn 5958 |
. . . . 5
⊢ (𝐹:(Base‘𝑀)⟶(Base‘𝑁) → 𝐹 Fn (Base‘𝑀)) |
47 | 37, 46 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐹 Fn (Base‘𝑀)) |
48 | | ffn 5958 |
. . . . 5
⊢ (𝐺:(Base‘𝑀)⟶(Base‘𝑁) → 𝐺 Fn (Base‘𝑀)) |
49 | 40, 48 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐺 Fn (Base‘𝑀)) |
50 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑀)
∈ V |
51 | 50 | a1i 11 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (Base‘𝑀) ∈ V) |
52 | 7 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑀 ∈ LMod) |
53 | 1, 4, 2, 6 | lmodvscl 18703 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ (Base‘𝑀)) |
54 | 52, 23, 24, 53 | syl3anc 1318 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠
‘𝑀)𝑦) ∈ (Base‘𝑀)) |
55 | | fnfvof 6809 |
. . . 4
⊢ (((𝐹 Fn (Base‘𝑀) ∧ 𝐺 Fn (Base‘𝑀)) ∧ ((Base‘𝑀) ∈ V ∧ (𝑥( ·𝑠
‘𝑀)𝑦) ∈ (Base‘𝑀))) → ((𝐹 ∘𝑓 + 𝐺)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = ((𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) + (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦)))) |
56 | 47, 49, 51, 54, 55 | syl22anc 1319 |
. . 3
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹 ∘𝑓 + 𝐺)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = ((𝐹‘(𝑥( ·𝑠
‘𝑀)𝑦)) + (𝐺‘(𝑥( ·𝑠
‘𝑀)𝑦)))) |
57 | | fnfvof 6809 |
. . . . 5
⊢ (((𝐹 Fn (Base‘𝑀) ∧ 𝐺 Fn (Base‘𝑀)) ∧ ((Base‘𝑀) ∈ V ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹 ∘𝑓 + 𝐺)‘𝑦) = ((𝐹‘𝑦) + (𝐺‘𝑦))) |
58 | 47, 49, 51, 24, 57 | syl22anc 1319 |
. . . 4
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹 ∘𝑓 + 𝐺)‘𝑦) = ((𝐹‘𝑦) + (𝐺‘𝑦))) |
59 | 58 | oveq2d 6565 |
. . 3
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠
‘𝑁)((𝐹 ∘𝑓
+ 𝐺)‘𝑦)) = (𝑥( ·𝑠
‘𝑁)((𝐹‘𝑦) + (𝐺‘𝑦)))) |
60 | 45, 56, 59 | 3eqtr4d 2654 |
. 2
⊢ (((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹 ∘𝑓 + 𝐺)‘(𝑥( ·𝑠
‘𝑀)𝑦)) = (𝑥( ·𝑠
‘𝑁)((𝐹 ∘𝑓
+ 𝐺)‘𝑦))) |
61 | 1, 2, 3, 4, 5, 6, 8, 10, 12, 21, 60 | islmhmd 18860 |
1
⊢ ((𝐹 ∈ (𝑀 LMHom 𝑁) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑀 LMHom 𝑁)) |