Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod1 20509 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
8 | 7 | adantr 482 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β LMod) |
9 | | lmhmlmod2 20508 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
10 | 9 | adantr 482 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β LMod) |
11 | 4, 5 | lmhmsca 20506 |
. . 3
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
12 | 11 | adantr 482 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (Scalarβπ) = (Scalarβπ)) |
13 | | lmodabl 20384 |
. . . 4
β’ (π β LMod β π β Abel) |
14 | 10, 13 | syl 17 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β Abel) |
15 | | lmghm 20507 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
16 | 15 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β πΉ β (π GrpHom π)) |
17 | | lmghm 20507 |
. . . 4
β’ (πΊ β (π LMHom π) β πΊ β (π GrpHom π)) |
18 | 17 | adantl 483 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β πΊ β (π GrpHom π)) |
19 | | lmhmplusg.p |
. . . 4
β’ + =
(+gβπ) |
20 | 19 | ghmplusg 19629 |
. . 3
β’ ((π β Abel β§ πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ βf + πΊ) β (π GrpHom π)) |
21 | 14, 16, 18, 20 | syl3anc 1372 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ βf + πΊ) β (π GrpHom π)) |
22 | | simpll 766 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΉ β (π LMHom π)) |
23 | | simprl 770 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
24 | | simprr 772 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π¦ β (Baseβπ)) |
25 | 4, 6, 1, 2, 3 | lmhmlin 20511 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
26 | 22, 23, 24, 25 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
27 | | simplr 768 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΊ β (π LMHom π)) |
28 | 4, 6, 1, 2, 3 | lmhmlin 20511 |
. . . . . 6
β’ ((πΊ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
29 | 27, 23, 24, 28 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
30 | 26, 29 | oveq12d 7376 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉβ(π₯( Β·π
βπ)π¦)) + (πΊβ(π₯( Β·π
βπ)π¦))) = ((π₯( Β·π
βπ)(πΉβπ¦)) + (π₯( Β·π
βπ)(πΊβπ¦)))) |
31 | 9 | ad2antrr 725 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β LMod) |
32 | 11 | fveq2d 6847 |
. . . . . . 7
β’ (πΉ β (π LMHom π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
33 | 32 | ad2antrr 725 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
34 | 23, 33 | eleqtrrd 2837 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
35 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
36 | 1, 35 | lmhmf 20510 |
. . . . . . 7
β’ (πΉ β (π LMHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
37 | 36 | ad2antrr 725 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
38 | 37, 24 | ffvelcdmd 7037 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβπ¦) β (Baseβπ)) |
39 | 1, 35 | lmhmf 20510 |
. . . . . . 7
β’ (πΊ β (π LMHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
40 | 39 | ad2antlr 726 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
41 | 40, 24 | ffvelcdmd 7037 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΊβπ¦) β (Baseβπ)) |
42 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
43 | 35, 19, 5, 3, 42 | lmodvsdi 20360 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ (πΉβπ¦) β (Baseβπ) β§ (πΊβπ¦) β (Baseβπ))) β (π₯( Β·π
βπ)((πΉβπ¦) + (πΊβπ¦))) = ((π₯( Β·π
βπ)(πΉβπ¦)) + (π₯( Β·π
βπ)(πΊβπ¦)))) |
44 | 31, 34, 38, 41, 43 | syl13anc 1373 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)((πΉβπ¦) + (πΊβπ¦))) = ((π₯( Β·π
βπ)(πΉβπ¦)) + (π₯( Β·π
βπ)(πΊβπ¦)))) |
45 | 30, 44 | eqtr4d 2776 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉβ(π₯( Β·π
βπ)π¦)) + (πΊβ(π₯( Β·π
βπ)π¦))) = (π₯( Β·π
βπ)((πΉβπ¦) + (πΊβπ¦)))) |
46 | 37 | ffnd 6670 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΉ Fn (Baseβπ)) |
47 | 40 | ffnd 6670 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΊ Fn (Baseβπ)) |
48 | | fvexd 6858 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Baseβπ) β V) |
49 | 7 | ad2antrr 725 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β LMod) |
50 | 1, 4, 2, 6 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
51 | 49, 23, 24, 50 | syl3anc 1372 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
52 | | fnfvof 7635 |
. . . 4
β’ (((πΉ Fn (Baseβπ) β§ πΊ Fn (Baseβπ)) β§ ((Baseβπ) β V β§ (π₯( Β·π
βπ)π¦) β (Baseβπ))) β ((πΉ βf + πΊ)β(π₯( Β·π
βπ)π¦)) = ((πΉβ(π₯( Β·π
βπ)π¦)) + (πΊβ(π₯( Β·π
βπ)π¦)))) |
53 | 46, 47, 48, 51, 52 | syl22anc 838 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ βf + πΊ)β(π₯( Β·π
βπ)π¦)) = ((πΉβ(π₯( Β·π
βπ)π¦)) + (πΊβ(π₯( Β·π
βπ)π¦)))) |
54 | | fnfvof 7635 |
. . . . 5
β’ (((πΉ Fn (Baseβπ) β§ πΊ Fn (Baseβπ)) β§ ((Baseβπ) β V β§ π¦ β (Baseβπ))) β ((πΉ βf + πΊ)βπ¦) = ((πΉβπ¦) + (πΊβπ¦))) |
55 | 46, 47, 48, 24, 54 | syl22anc 838 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ βf + πΊ)βπ¦) = ((πΉβπ¦) + (πΊβπ¦))) |
56 | 55 | oveq2d 7374 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)((πΉ βf + πΊ)βπ¦)) = (π₯( Β·π
βπ)((πΉβπ¦) + (πΊβπ¦)))) |
57 | 45, 53, 56 | 3eqtr4d 2783 |
. 2
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ βf + πΊ)β(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)((πΉ βf + πΊ)βπ¦))) |
58 | 1, 2, 3, 4, 5, 6, 8, 10, 12, 21, 57 | islmhmd 20515 |
1
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ βf + πΊ) β (π LMHom π)) |