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 | 3ad2ant1 1134 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β π β LMod) |
9 | | simp2 1138 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β π β LMod) |
10 | | reslmhm2.u |
. . . . 5
β’ π = (π βΎs π) |
11 | 10, 5 | resssca 17229 |
. . . 4
β’ (π β πΏ β (Scalarβπ) = (Scalarβπ)) |
12 | 11 | 3ad2ant3 1136 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β (Scalarβπ) = (Scalarβπ)) |
13 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
14 | 4, 13 | lmhmsca 20506 |
. . . 4
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
15 | 14 | 3ad2ant1 1134 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β (Scalarβπ) = (Scalarβπ)) |
16 | 12, 15 | eqtrd 2773 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β (Scalarβπ) = (Scalarβπ)) |
17 | | lmghm 20507 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
18 | 17 | 3ad2ant1 1134 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β πΉ β (π GrpHom π)) |
19 | | reslmhm2.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
20 | 19 | lsssubg 20433 |
. . . 4
β’ ((π β LMod β§ π β πΏ) β π β (SubGrpβπ)) |
21 | 20 | 3adant1 1131 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β π β (SubGrpβπ)) |
22 | 10 | resghm2 19030 |
. . 3
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β πΉ β (π GrpHom π)) |
23 | 18, 21, 22 | syl2anc 585 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β πΉ β (π GrpHom π)) |
24 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
25 | 4, 6, 1, 2, 24 | lmhmlin 20511 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
26 | 25 | 3expb 1121 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
27 | 26 | 3ad2antl1 1186 |
. . 3
β’ (((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
28 | | simpl3 1194 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β πΏ) |
29 | 10, 3 | ressvsca 17230 |
. . . . 5
β’ (π β πΏ β (
Β·π βπ) = ( Β·π
βπ)) |
30 | 29 | oveqd 7375 |
. . . 4
β’ (π β πΏ β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
31 | 28, 30 | syl 17 |
. . 3
β’ (((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
32 | 27, 31 | eqtr4d 2776 |
. 2
β’ (((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
33 | 1, 2, 3, 4, 5, 6, 8, 9, 16, 23, 32 | islmhmd 20515 |
1
β’ ((πΉ β (π LMHom π) β§ π β LMod β§ π β πΏ) β πΉ β (π LMHom π)) |