Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2731 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2731 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2731 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2731 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2731 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod1 20789 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
8 | 7 | adantl 481 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
9 | | simpl1 1190 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
10 | | simpl2 1191 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β πΏ) |
11 | | reslmhm2.u |
. . . . 5
β’ π = (π βΎs π) |
12 | | reslmhm2.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
13 | 11, 12 | lsslmod 20716 |
. . . 4
β’ ((π β LMod β§ π β πΏ) β π β LMod) |
14 | 9, 10, 13 | syl2anc 583 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
15 | | eqid 2731 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
16 | 11, 15 | resssca 17293 |
. . . . 5
β’ (π β πΏ β (Scalarβπ) = (Scalarβπ)) |
17 | 16 | 3ad2ant2 1133 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (Scalarβπ) = (Scalarβπ)) |
18 | 4, 15 | lmhmsca 20786 |
. . . 4
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
19 | 17, 18 | sylan9req 2792 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β (Scalarβπ) = (Scalarβπ)) |
20 | | lmghm 20787 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
21 | 12 | lsssubg 20713 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ) β π β (SubGrpβπ)) |
22 | 11 | resghm2b 19149 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ ran πΉ β π) β (πΉ β (π GrpHom π) β πΉ β (π GrpHom π))) |
23 | 21, 22 | stoic3 1777 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (πΉ β (π GrpHom π) β πΉ β (π GrpHom π))) |
24 | 23 | biimpa 476 |
. . . 4
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π GrpHom π)) β πΉ β (π GrpHom π)) |
25 | 20, 24 | sylan2 592 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π GrpHom π)) |
26 | | eqid 2731 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
27 | 4, 6, 1, 2, 26 | lmhmlin 20791 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
28 | 27 | 3expb 1119 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
29 | 28 | adantll 711 |
. . . 4
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
30 | | simpll2 1212 |
. . . . 5
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β πΏ) |
31 | 11, 26 | ressvsca 17294 |
. . . . . 6
β’ (π β πΏ β (
Β·π βπ) = ( Β·π
βπ)) |
32 | 31 | oveqd 7429 |
. . . . 5
β’ (π β πΏ β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
33 | 30, 32 | syl 17 |
. . . 4
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
34 | 29, 33 | eqtrd 2771 |
. . 3
β’ ((((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
35 | 1, 2, 3, 4, 5, 6, 8, 14, 19, 25, 34 | islmhmd 20795 |
. 2
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
36 | | simpr 484 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
37 | | simpl1 1190 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β LMod) |
38 | | simpl2 1191 |
. . 3
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β π β πΏ) |
39 | 11, 12 | reslmhm2 20809 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β πΉ β (π LMHom π)) |
40 | 36, 37, 38, 39 | syl3anc 1370 |
. 2
β’ (((π β LMod β§ π β πΏ β§ ran πΉ β π) β§ πΉ β (π LMHom π)) β πΉ β (π LMHom π)) |
41 | 35, 40 | impbida 798 |
1
β’ ((π β LMod β§ π β πΏ β§ ran πΉ β π) β (πΉ β (π LMHom π) β πΉ β (π LMHom π))) |