Step | Hyp | Ref
| Expression |
1 | | lmhmvsca.v |
. 2
β’ π = (Baseβπ) |
2 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | lmhmvsca.s |
. 2
β’ Β· = (
Β·π βπ) |
4 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | lmhmvsca.j |
. 2
β’ π½ = (Scalarβπ) |
6 | | eqid 2733 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod1 20509 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
8 | 7 | 3ad2ant3 1136 |
. 2
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β π β LMod) |
9 | | lmhmlmod2 20508 |
. . 3
β’ (πΉ β (π LMHom π) β π β LMod) |
10 | 9 | 3ad2ant3 1136 |
. 2
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β π β LMod) |
11 | 4, 5 | lmhmsca 20506 |
. . 3
β’ (πΉ β (π LMHom π) β π½ = (Scalarβπ)) |
12 | 11 | 3ad2ant3 1136 |
. 2
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β π½ = (Scalarβπ)) |
13 | 1 | fvexi 6857 |
. . . . . 6
β’ π β V |
14 | 13 | a1i 11 |
. . . . 5
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β π β V) |
15 | | simpl2 1193 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ π£ β π) β π΄ β πΎ) |
16 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
17 | 1, 16 | lmhmf 20510 |
. . . . . . 7
β’ (πΉ β (π LMHom π) β πΉ:πβΆ(Baseβπ)) |
18 | 17 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β πΉ:πβΆ(Baseβπ)) |
19 | 18 | ffvelcdmda 7036 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ π£ β π) β (πΉβπ£) β (Baseβπ)) |
20 | | fconstmpt 5695 |
. . . . . 6
β’ (π Γ {π΄}) = (π£ β π β¦ π΄) |
21 | 20 | a1i 11 |
. . . . 5
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β (π Γ {π΄}) = (π£ β π β¦ π΄)) |
22 | 18 | feqmptd 6911 |
. . . . 5
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β πΉ = (π£ β π β¦ (πΉβπ£))) |
23 | 14, 15, 19, 21, 22 | offval2 7638 |
. . . 4
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π Γ {π΄}) βf Β· πΉ) = (π£ β π β¦ (π΄ Β· (πΉβπ£)))) |
24 | | eqidd 2734 |
. . . . 5
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β (π’ β (Baseβπ) β¦ (π΄ Β· π’)) = (π’ β (Baseβπ) β¦ (π΄ Β· π’))) |
25 | | oveq2 7366 |
. . . . 5
β’ (π’ = (πΉβπ£) β (π΄ Β· π’) = (π΄ Β· (πΉβπ£))) |
26 | 19, 22, 24, 25 | fmptco 7076 |
. . . 4
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π’ β (Baseβπ) β¦ (π΄ Β· π’)) β πΉ) = (π£ β π β¦ (π΄ Β· (πΉβπ£)))) |
27 | 23, 26 | eqtr4d 2776 |
. . 3
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π Γ {π΄}) βf Β· πΉ) = ((π’ β (Baseβπ) β¦ (π΄ Β· π’)) β πΉ)) |
28 | | simp2 1138 |
. . . . 5
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β π΄ β πΎ) |
29 | | lmhmvsca.k |
. . . . . 6
β’ πΎ = (Baseβπ½) |
30 | 16, 5, 3, 29 | lmodvsghm 20398 |
. . . . 5
β’ ((π β LMod β§ π΄ β πΎ) β (π’ β (Baseβπ) β¦ (π΄ Β· π’)) β (π GrpHom π)) |
31 | 10, 28, 30 | syl2anc 585 |
. . . 4
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β (π’ β (Baseβπ) β¦ (π΄ Β· π’)) β (π GrpHom π)) |
32 | | lmghm 20507 |
. . . . 5
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
33 | 32 | 3ad2ant3 1136 |
. . . 4
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β πΉ β (π GrpHom π)) |
34 | | ghmco 19033 |
. . . 4
β’ (((π’ β (Baseβπ) β¦ (π΄ Β· π’)) β (π GrpHom π) β§ πΉ β (π GrpHom π)) β ((π’ β (Baseβπ) β¦ (π΄ Β· π’)) β πΉ) β (π GrpHom π)) |
35 | 31, 33, 34 | syl2anc 585 |
. . 3
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π’ β (Baseβπ) β¦ (π΄ Β· π’)) β πΉ) β (π GrpHom π)) |
36 | 27, 35 | eqeltrd 2834 |
. 2
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π Γ {π΄}) βf Β· πΉ) β (π GrpHom π)) |
37 | | simpl1 1192 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π½ β CRing) |
38 | | simpl2 1193 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π΄ β πΎ) |
39 | | simprl 770 |
. . . . . . 7
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π₯ β (Baseβ(Scalarβπ))) |
40 | 12 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β (Baseβπ½) = (Baseβ(Scalarβπ))) |
41 | 29, 40 | eqtrid 2785 |
. . . . . . . 8
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β πΎ = (Baseβ(Scalarβπ))) |
42 | 41 | adantr 482 |
. . . . . . 7
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β πΎ = (Baseβ(Scalarβπ))) |
43 | 39, 42 | eleqtrrd 2837 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π₯ β πΎ) |
44 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ½) = (.rβπ½) |
45 | 29, 44 | crngcom 19987 |
. . . . . 6
β’ ((π½ β CRing β§ π΄ β πΎ β§ π₯ β πΎ) β (π΄(.rβπ½)π₯) = (π₯(.rβπ½)π΄)) |
46 | 37, 38, 43, 45 | syl3anc 1372 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π΄(.rβπ½)π₯) = (π₯(.rβπ½)π΄)) |
47 | 46 | oveq1d 7373 |
. . . 4
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β ((π΄(.rβπ½)π₯) Β· (πΉβπ¦)) = ((π₯(.rβπ½)π΄) Β· (πΉβπ¦))) |
48 | 10 | adantr 482 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π β LMod) |
49 | 18 | adantr 482 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β πΉ:πβΆ(Baseβπ)) |
50 | | simprr 772 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π¦ β π) |
51 | 49, 50 | ffvelcdmd 7037 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (πΉβπ¦) β (Baseβπ)) |
52 | 16, 5, 3, 29, 44 | lmodvsass 20362 |
. . . . 5
β’ ((π β LMod β§ (π΄ β πΎ β§ π₯ β πΎ β§ (πΉβπ¦) β (Baseβπ))) β ((π΄(.rβπ½)π₯) Β· (πΉβπ¦)) = (π΄ Β· (π₯ Β· (πΉβπ¦)))) |
53 | 48, 38, 43, 51, 52 | syl13anc 1373 |
. . . 4
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β ((π΄(.rβπ½)π₯) Β· (πΉβπ¦)) = (π΄ Β· (π₯ Β· (πΉβπ¦)))) |
54 | 16, 5, 3, 29, 44 | lmodvsass 20362 |
. . . . 5
β’ ((π β LMod β§ (π₯ β πΎ β§ π΄ β πΎ β§ (πΉβπ¦) β (Baseβπ))) β ((π₯(.rβπ½)π΄) Β· (πΉβπ¦)) = (π₯ Β· (π΄ Β· (πΉβπ¦)))) |
55 | 48, 43, 38, 51, 54 | syl13anc 1373 |
. . . 4
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β ((π₯(.rβπ½)π΄) Β· (πΉβπ¦)) = (π₯ Β· (π΄ Β· (πΉβπ¦)))) |
56 | 47, 53, 55 | 3eqtr3d 2781 |
. . 3
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π΄ Β· (π₯ Β· (πΉβπ¦))) = (π₯ Β· (π΄ Β· (πΉβπ¦)))) |
57 | 1, 4, 2, 6 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π) β (π₯( Β·π
βπ)π¦) β π) |
58 | 57 | 3expb 1121 |
. . . . 5
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π)) β (π₯( Β·π
βπ)π¦) β π) |
59 | 8, 58 | sylan 581 |
. . . 4
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π₯( Β·π
βπ)π¦) β π) |
60 | 13 | a1i 11 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β π β V) |
61 | 18 | ffnd 6670 |
. . . . . 6
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β πΉ Fn π) |
62 | 61 | adantr 482 |
. . . . 5
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β πΉ Fn π) |
63 | 4, 6, 1, 2, 3 | lmhmlin 20511 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯ Β· (πΉβπ¦))) |
64 | 63 | 3expb 1121 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯ Β· (πΉβπ¦))) |
65 | 64 | 3ad2antl3 1188 |
. . . . . 6
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯ Β· (πΉβπ¦))) |
66 | 65 | adantr 482 |
. . . . 5
β’ ((((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β§ (π₯( Β·π
βπ)π¦) β π) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯ Β· (πΉβπ¦))) |
67 | 60, 38, 62, 66 | ofc1 7644 |
. . . 4
β’ ((((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β§ (π₯( Β·π
βπ)π¦) β π) β (((π Γ {π΄}) βf Β· πΉ)β(π₯( Β·π
βπ)π¦)) = (π΄ Β· (π₯ Β· (πΉβπ¦)))) |
68 | 59, 67 | mpdan 686 |
. . 3
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (((π Γ {π΄}) βf Β· πΉ)β(π₯( Β·π
βπ)π¦)) = (π΄ Β· (π₯ Β· (πΉβπ¦)))) |
69 | | eqidd 2734 |
. . . . . 6
β’ ((((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β§ π¦ β π) β (πΉβπ¦) = (πΉβπ¦)) |
70 | 60, 38, 62, 69 | ofc1 7644 |
. . . . 5
β’ ((((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β§ π¦ β π) β (((π Γ {π΄}) βf Β· πΉ)βπ¦) = (π΄ Β· (πΉβπ¦))) |
71 | 50, 70 | mpdan 686 |
. . . 4
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (((π Γ {π΄}) βf Β· πΉ)βπ¦) = (π΄ Β· (πΉβπ¦))) |
72 | 71 | oveq2d 7374 |
. . 3
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (π₯ Β· (((π Γ {π΄}) βf Β· πΉ)βπ¦)) = (π₯ Β· (π΄ Β· (πΉβπ¦)))) |
73 | 56, 68, 72 | 3eqtr4d 2783 |
. 2
β’ (((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β§ (π₯ β (Baseβ(Scalarβπ)) β§ π¦ β π)) β (((π Γ {π΄}) βf Β· πΉ)β(π₯( Β·π
βπ)π¦)) = (π₯ Β· (((π Γ {π΄}) βf Β· πΉ)βπ¦))) |
74 | 1, 2, 3, 4, 5, 6, 8, 10, 12, 36, 73 | islmhmd 20515 |
1
β’ ((π½ β CRing β§ π΄ β πΎ β§ πΉ β (π LMHom π)) β ((π Γ {π΄}) βf Β· πΉ) β (π LMHom π)) |