Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod1 20509 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
8 | 7 | adantl 483 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
9 | | simpl1 1192 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
10 | | simpl2 1193 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β πΏ) |
11 | | reslmhm2.u |
. . . . 5
β’ π = (π βΎs π) |
12 | | reslmhm2.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
13 | 11, 12 | lsslmod 20436 |
. . . 4
β’ ((π β LMod β§ π β πΏ) β π β LMod) |
14 | 9, 10, 13 | syl2anc 585 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
15 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
16 | 11, 15 | resssca 17229 |
. . . . 5
β’ (π β πΏ β (Scalarβπ) = (Scalarβπ)) |
17 | 16 | 3ad2ant2 1135 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (Scalarβπ) = (Scalarβπ)) |
18 | 4, 15 | lmhmsca 20506 |
. . . 4
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
19 | 17, 18 | sylan9req 2794 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β (Scalarβπ) = (Scalarβπ)) |
20 | | lmghm 20507 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
21 | 12 | lsssubg 20433 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ) β π β (SubGrpβπ)) |
22 | 11 | resghm2b 19031 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ ran πΉ β π) β (πΉ β (π GrpHom π) β πΉ β (π GrpHom π))) |
23 | 21, 22 | stoic3 1779 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (πΉ β (π GrpHom π) β πΉ β (π GrpHom π))) |
24 | 23 | biimpa 478 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π GrpHom π)) β πΉ β (π GrpHom π)) |
25 | 20, 24 | sylan2 594 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π GrpHom π)) |
26 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
27 | 4, 6, 1, 2, 26 | lmhmlin 20511 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
28 | 27 | 3expb 1121 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
29 | 28 | adantll 713 |
. . . 4
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
30 | | simpll2 1214 |
. . . . 5
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β πΏ) |
31 | 11, 26 | ressvsca 17230 |
. . . . . 6
β’ (π β πΏ β (
Β·π βπ) = ( Β·π
βπ)) |
32 | 31 | oveqd 7375 |
. . . . 5
β’ (π β πΏ β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
33 | 30, 32 | syl 17 |
. . . 4
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
34 | 29, 33 | eqtrd 2773 |
. . 3
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
35 | 1, 2, 3, 4, 5, 6, 8, 14, 19, 25, 34 | islmhmd 20515 |
. 2
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
36 | | simpr 486 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
37 | | simpl1 1192 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
38 | | simpl2 1193 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β πΏ) |
39 | 11, 12 | reslmhm2 20529 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β πΉ β (π LMHom π)) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. 2
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
41 | 35, 40 | impbida 800 |
1
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (πΉ β (π LMHom π) β πΉ β (π LMHom π))) |