Step | Hyp | Ref
| Expression |
1 | | lmhmlmod1 20509 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
2 | | reslmhm.r |
. . . 4
β’ π
= (π βΎs π) |
3 | | reslmhm.u |
. . . 4
β’ π = (LSubSpβπ) |
4 | 2, 3 | lsslmod 20436 |
. . 3
β’ ((π β LMod β§ π β π) β π
β LMod) |
5 | 1, 4 | sylan 581 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β π
β LMod) |
6 | | lmhmlmod2 20508 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
7 | 6 | adantr 482 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
8 | | lmghm 20507 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
9 | 3 | lsssubg 20433 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
10 | 1, 9 | sylan 581 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (SubGrpβπ)) |
11 | 2 | resghm 19029 |
. . . 4
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ βΎ π) β (π
GrpHom π)) |
12 | 8, 10, 11 | syl2an2r 684 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ βΎ π) β (π
GrpHom π)) |
13 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
14 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
15 | 13, 14 | lmhmsca 20506 |
. . . 4
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
16 | 2, 13 | resssca 17229 |
. . . 4
β’ (π β π β (Scalarβπ) = (Scalarβπ
)) |
17 | 15, 16 | sylan9eq 2793 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β (Scalarβπ) = (Scalarβπ
)) |
18 | | simpll 766 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β πΉ β (π LMHom π)) |
19 | | simprl 770 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β (Baseβ(Scalarβπ))) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
21 | 20, 3 | lssss 20412 |
. . . . . . . . . 10
β’ (π β π β π β (Baseβπ)) |
22 | 21 | adantl 483 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (Baseβπ)) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β (Baseβπ)) |
24 | 2, 20 | ressbas2 17125 |
. . . . . . . . . . . 12
β’ (π β (Baseβπ) β π = (Baseβπ
)) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . 11
β’ ((πΉ β (π LMHom π) β§ π β π) β π = (Baseβπ
)) |
26 | 25 | eleq2d 2820 |
. . . . . . . . . 10
β’ ((πΉ β (π LMHom π) β§ π β π) β (π β π β π β (Baseβπ
))) |
27 | 26 | biimpar 479 |
. . . . . . . . 9
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβπ
)) β π β π) |
28 | 27 | adantrl 715 |
. . . . . . . 8
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β π) |
29 | 23, 28 | sseldd 3946 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β (Baseβπ)) |
30 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
31 | | eqid 2733 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
32 | | eqid 2733 |
. . . . . . . 8
β’ (
Β·π βπ) = ( Β·π
βπ) |
33 | 13, 30, 20, 31, 32 | lmhmlin 20511 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ)) β (πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(πΉβπ))) |
34 | 18, 19, 29, 33 | syl3anc 1372 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β (πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(πΉβπ))) |
35 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β LMod) |
37 | | simplr 768 |
. . . . . . . 8
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β π β π) |
38 | 13, 31, 30, 3 | lssvscl 20431 |
. . . . . . . 8
β’ (((π β LMod β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)π) β π) |
39 | 36, 37, 19, 28, 38 | syl22anc 838 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β (π( Β·π
βπ)π) β π) |
40 | 39 | fvresd 6863 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β ((πΉ βΎ π)β(π( Β·π
βπ)π)) = (πΉβ(π( Β·π
βπ)π))) |
41 | | fvres 6862 |
. . . . . . . 8
β’ (π β π β ((πΉ βΎ π)βπ) = (πΉβπ)) |
42 | 41 | oveq2d 7374 |
. . . . . . 7
β’ (π β π β (π( Β·π
βπ)((πΉ βΎ π)βπ)) = (π( Β·π
βπ)(πΉβπ))) |
43 | 28, 42 | syl 17 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β (π( Β·π
βπ)((πΉ βΎ π)βπ)) = (π( Β·π
βπ)(πΉβπ))) |
44 | 34, 40, 43 | 3eqtr4d 2783 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ
))) β ((πΉ βΎ π)β(π( Β·π
βπ)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ))) |
45 | 44 | ralrimivva 3194 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β βπ β (Baseβ(Scalarβπ))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ))) |
46 | 16 | adantl 483 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β (Scalarβπ) = (Scalarβπ
)) |
47 | 46 | fveq2d 6847 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ
))) |
48 | 2, 31 | ressvsca 17230 |
. . . . . . . . 9
β’ (π β π β (
Β·π βπ) = ( Β·π
βπ
)) |
49 | 48 | adantl 483 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ π β π) β (
Β·π βπ) = ( Β·π
βπ
)) |
50 | 49 | oveqd 7375 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β π) β (π( Β·π
βπ)π) = (π( Β·π
βπ
)π)) |
51 | 50 | fveqeq2d 6851 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β (((πΉ βΎ π)β(π( Β·π
βπ)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)) β ((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)))) |
52 | 51 | ralbidv 3171 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π β π) β (βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)) β βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)))) |
53 | 47, 52 | raleqbidv 3318 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β (βπ β (Baseβ(Scalarβπ))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)) β βπ β (Baseβ(Scalarβπ
))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)))) |
54 | 45, 53 | mpbid 231 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β βπ β (Baseβ(Scalarβπ
))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ))) |
55 | 12, 17, 54 | 3jca 1129 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β ((πΉ βΎ π) β (π
GrpHom π) β§ (Scalarβπ) = (Scalarβπ
) β§ βπ β (Baseβ(Scalarβπ
))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ)))) |
56 | | eqid 2733 |
. . 3
β’
(Scalarβπ
) =
(Scalarβπ
) |
57 | | eqid 2733 |
. . 3
β’
(Baseβ(Scalarβπ
)) = (Baseβ(Scalarβπ
)) |
58 | | eqid 2733 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
59 | | eqid 2733 |
. . 3
β’ (
Β·π βπ
) = ( Β·π
βπ
) |
60 | 56, 14, 57, 58, 59, 32 | islmhm 20503 |
. 2
β’ ((πΉ βΎ π) β (π
LMHom π) β ((π
β LMod β§ π β LMod) β§ ((πΉ βΎ π) β (π
GrpHom π) β§ (Scalarβπ) = (Scalarβπ
) β§ βπ β (Baseβ(Scalarβπ
))βπ β (Baseβπ
)((πΉ βΎ π)β(π( Β·π
βπ
)π)) = (π( Β·π
βπ)((πΉ βΎ π)βπ))))) |
61 | 5, 7, 55, 60 | syl21anbrc 1345 |
1
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ βΎ π) β (π
LMHom π)) |