Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2736 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2736 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2736 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2736 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2736 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod1 20340 |
. . 3
β’ (πΊ β (π LMHom π) β π β LMod) |
8 | 7 | adantl 483 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β LMod) |
9 | | lmhmlmod2 20339 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
10 | 9 | adantr 482 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β LMod) |
11 | | eqid 2736 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
12 | 11, 5 | lmhmsca 20337 |
. . 3
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
13 | 4, 11 | lmhmsca 20337 |
. . 3
β’ (πΊ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
14 | 12, 13 | sylan9eq 2796 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (Scalarβπ) = (Scalarβπ)) |
15 | | lmghm 20338 |
. . 3
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
16 | | lmghm 20338 |
. . 3
β’ (πΊ β (π LMHom π) β πΊ β (π GrpHom π)) |
17 | | ghmco 18899 |
. . 3
β’ ((πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ β πΊ) β (π GrpHom π)) |
18 | 15, 16, 17 | syl2an 597 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ β πΊ) β (π GrpHom π)) |
19 | | simplr 767 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΊ β (π LMHom π)) |
20 | | simprl 769 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
21 | | simprr 771 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π¦ β (Baseβπ)) |
22 | | eqid 2736 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
23 | 4, 6, 1, 2, 22 | lmhmlin 20342 |
. . . . . 6
β’ ((πΊ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
24 | 19, 20, 21, 23 | syl3anc 1371 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
25 | 24 | fveq2d 6808 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(πΊβ(π₯( Β·π
βπ)π¦))) = (πΉβ(π₯( Β·π
βπ)(πΊβπ¦)))) |
26 | | simpll 765 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β πΉ β (π LMHom π)) |
27 | 13 | fveq2d 6808 |
. . . . . . 7
β’ (πΊ β (π LMHom π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
28 | 27 | ad2antlr 725 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
29 | 20, 28 | eleqtrrd 2840 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π₯ β (Baseβ(Scalarβπ))) |
30 | | eqid 2736 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
31 | 1, 30 | lmhmf 20341 |
. . . . . . . 8
β’ (πΊ β (π LMHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
32 | 31 | adantl 483 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
33 | 32 | ffvelcdmda 6993 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π¦ β (Baseβπ)) β (πΊβπ¦) β (Baseβπ)) |
34 | 33 | adantrl 714 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΊβπ¦) β (Baseβπ)) |
35 | | eqid 2736 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
36 | 11, 35, 30, 22, 3 | lmhmlin 20342 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ (πΊβπ¦) β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)(πΊβπ¦))) = (π₯( Β·π
βπ)(πΉβ(πΊβπ¦)))) |
37 | 26, 29, 34, 36 | syl3anc 1371 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(π₯( Β·π
βπ)(πΊβπ¦))) = (π₯( Β·π
βπ)(πΉβ(πΊβπ¦)))) |
38 | 25, 37 | eqtrd 2776 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (πΉβ(πΊβ(π₯( Β·π
βπ)π¦))) = (π₯( Β·π
βπ)(πΉβ(πΊβπ¦)))) |
39 | 32 | ffnd 6631 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β πΊ Fn (Baseβπ)) |
40 | 7 | ad2antlr 725 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β π β LMod) |
41 | 1, 4, 2, 6 | lmodvscl 20185 |
. . . . 5
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
42 | 40, 20, 21, 41 | syl3anc 1371 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
43 | | fvco2 6897 |
. . . 4
β’ ((πΊ Fn (Baseβπ) β§ (π₯( Β·π
βπ)π¦) β (Baseβπ)) β ((πΉ β πΊ)β(π₯( Β·π
βπ)π¦)) = (πΉβ(πΊβ(π₯( Β·π
βπ)π¦)))) |
44 | 39, 42, 43 | syl2an2r 683 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ β πΊ)β(π₯( Β·π
βπ)π¦)) = (πΉβ(πΊβ(π₯( Β·π
βπ)π¦)))) |
45 | | fvco2 6897 |
. . . . 5
β’ ((πΊ Fn (Baseβπ) β§ π¦ β (Baseβπ)) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
46 | 39, 21, 45 | syl2an2r 683 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
47 | 46 | oveq2d 7323 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β (π₯( Β·π
βπ)((πΉ β πΊ)βπ¦)) = (π₯( Β·π
βπ)(πΉβ(πΊβπ¦)))) |
48 | 38, 44, 47 | 3eqtr4d 2786 |
. 2
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ))) β ((πΉ β πΊ)β(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)((πΉ β πΊ)βπ¦))) |
49 | 1, 2, 3, 4, 5, 6, 8, 10, 14, 18, 48 | islmhmd 20346 |
1
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (πΉ β πΊ) β (π LMHom π)) |