Step | Hyp | Ref
| Expression |
1 | | lmghm 20507 |
. . 3
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
2 | | lmhmlmod1 20509 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
3 | | simpr 486 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ π β π) β π β π) |
4 | | lmhmima.x |
. . . . 5
β’ π = (LSubSpβπ) |
5 | 4 | lsssubg 20433 |
. . . 4
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
6 | 2, 3, 5 | syl2an2r 684 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (SubGrpβπ)) |
7 | | ghmima 19034 |
. . 3
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ β π) β (SubGrpβπ)) |
8 | 1, 6, 7 | syl2an2r 684 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β (SubGrpβπ)) |
9 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
10 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
11 | 9, 10 | lmhmf 20510 |
. . . . . . . . 9
β’ (πΉ β (π LMHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ π β π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
13 | | ffn 6669 |
. . . . . . . 8
β’ (πΉ:(Baseβπ)βΆ(Baseβπ) β πΉ Fn (Baseβπ)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β π) β πΉ Fn (Baseβπ)) |
15 | 9, 4 | lssss 20412 |
. . . . . . . 8
β’ (π β π β π β (Baseβπ)) |
16 | 3, 15 | syl 17 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ π β π) β π β (Baseβπ)) |
17 | 14, 16 | fvelimabd 6916 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β π) β (π β (πΉ β π) β βπ β π (πΉβπ) = π)) |
18 | 17 | adantr 482 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (π β (πΉ β π) β βπ β π (πΉβπ) = π)) |
19 | | simpll 766 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β πΉ β (π LMHom π)) |
20 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(Scalarβπ) =
(Scalarβπ) |
21 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(Scalarβπ) =
(Scalarβπ) |
22 | 20, 21 | lmhmsca 20506 |
. . . . . . . . . . . . . . 15
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π LMHom π) β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
24 | 23 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((πΉ β (π LMHom π) β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
25 | 24 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ ((πΉ β (π LMHom π) β§ π β π) β (π β (Baseβ(Scalarβπ)) β π β (Baseβ(Scalarβπ)))) |
26 | 25 | biimpa 478 |
. . . . . . . . . . 11
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
27 | 26 | adantrr 716 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β (Baseβ(Scalarβπ))) |
28 | 16 | sselda 3945 |
. . . . . . . . . . 11
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β π) β π β (Baseβπ)) |
29 | 28 | adantrl 715 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β (Baseβπ)) |
30 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
31 | | eqid 2733 |
. . . . . . . . . . 11
β’ (
Β·π βπ) = ( Β·π
βπ) |
32 | | eqid 2733 |
. . . . . . . . . . 11
β’ (
Β·π βπ) = ( Β·π
βπ) |
33 | 20, 30, 9, 31, 32 | lmhmlin 20511 |
. . . . . . . . . 10
β’ ((πΉ β (π LMHom π) β§ π β (Baseβ(Scalarβπ)) β§ π β (Baseβπ)) β (πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(πΉβπ))) |
34 | 19, 27, 29, 33 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(πΉβπ))) |
35 | 19, 11, 13 | 3syl 18 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β πΉ Fn (Baseβπ)) |
36 | | simplr 768 |
. . . . . . . . . . 11
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β π) |
37 | 36, 15 | syl 17 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β (Baseβπ)) |
38 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
39 | 38 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β LMod) |
40 | | simprr 772 |
. . . . . . . . . . 11
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β π) |
41 | 20, 31, 30, 4 | lssvscl 20431 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)π) β π) |
42 | 39, 36, 27, 40, 41 | syl22anc 838 |
. . . . . . . . . 10
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)π) β π) |
43 | | fnfvima 7184 |
. . . . . . . . . 10
β’ ((πΉ Fn (Baseβπ) β§ π β (Baseβπ) β§ (π( Β·π
βπ)π) β π) β (πΉβ(π( Β·π
βπ)π)) β (πΉ β π)) |
44 | 35, 37, 42, 43 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (πΉβ(π( Β·π
βπ)π)) β (πΉ β π)) |
45 | 34, 44 | eqeltrrd 2835 |
. . . . . . . 8
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)(πΉβπ)) β (πΉ β π)) |
46 | 45 | anassrs 469 |
. . . . . . 7
β’ ((((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ π β π) β (π( Β·π
βπ)(πΉβπ)) β (πΉ β π)) |
47 | | oveq2 7366 |
. . . . . . . 8
β’ ((πΉβπ) = π β (π( Β·π
βπ)(πΉβπ)) = (π( Β·π
βπ)π)) |
48 | 47 | eleq1d 2819 |
. . . . . . 7
β’ ((πΉβπ) = π β ((π( Β·π
βπ)(πΉβπ)) β (πΉ β π) β (π( Β·π
βπ)π) β (πΉ β π))) |
49 | 46, 48 | syl5ibcom 244 |
. . . . . 6
β’ ((((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β§ π β π) β ((πΉβπ) = π β (π( Β·π
βπ)π) β (πΉ β π))) |
50 | 49 | rexlimdva 3149 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (βπ β π (πΉβπ) = π β (π( Β·π
βπ)π) β (πΉ β π))) |
51 | 18, 50 | sylbid 239 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ π β π) β§ π β (Baseβ(Scalarβπ))) β (π β (πΉ β π) β (π( Β·π
βπ)π) β (πΉ β π))) |
52 | 51 | impr 456 |
. . 3
β’ (((πΉ β (π LMHom π) β§ π β π) β§ (π β (Baseβ(Scalarβπ)) β§ π β (πΉ β π))) β (π( Β·π
βπ)π) β (πΉ β π)) |
53 | 52 | ralrimivva 3194 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β βπ β (Baseβ(Scalarβπ))βπ β (πΉ β π)(π( Β·π
βπ)π) β (πΉ β π)) |
54 | | lmhmlmod2 20508 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
55 | 54 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ π β π) β π β LMod) |
56 | | eqid 2733 |
. . . 4
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
57 | | lmhmima.y |
. . . 4
β’ π = (LSubSpβπ) |
58 | 21, 56, 10, 32, 57 | islss4 20438 |
. . 3
β’ (π β LMod β ((πΉ β π) β π β ((πΉ β π) β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ β (πΉ β π)(π( Β·π
βπ)π) β (πΉ β π)))) |
59 | 55, 58 | syl 17 |
. 2
β’ ((πΉ β (π LMHom π) β§ π β π) β ((πΉ β π) β π β ((πΉ β π) β (SubGrpβπ) β§ βπ β (Baseβ(Scalarβπ))βπ β (πΉ β π)(π( Β·π
βπ)π) β (πΉ β π)))) |
60 | 8, 53, 59 | mpbir2and 712 |
1
β’ ((πΉ β (π LMHom π) β§ π β π) β (πΉ β π) β π) |