Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
β’ π΄ = (MEndoβπ) |
2 | 1 | mendbas 41912 |
. . 3
β’ (π LMHom π) = (Baseβπ΄) |
3 | 2 | a1i 11 |
. 2
β’ (π β LMod β (π LMHom π) = (Baseβπ΄)) |
4 | | eqidd 2734 |
. 2
β’ (π β LMod β
(+gβπ΄) =
(+gβπ΄)) |
5 | | eqidd 2734 |
. 2
β’ (π β LMod β
(.rβπ΄) =
(.rβπ΄)) |
6 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(+gβπ΄) = (+gβπ΄) |
8 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(+gβπ΄)π¦) = (π₯ βf
(+gβπ)π¦)) |
9 | 6 | lmhmplusg 20648 |
. . . . 5
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯ βf
(+gβπ)π¦) β (π LMHom π)) |
10 | 8, 9 | eqeltrd 2834 |
. . . 4
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(+gβπ΄)π¦) β (π LMHom π)) |
11 | 10 | 3adant1 1131 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(+gβπ΄)π¦) β (π LMHom π)) |
12 | | simpr1 1195 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯ β (π LMHom π)) |
13 | | simpr2 1196 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦ β (π LMHom π)) |
14 | 12, 13, 9 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯ βf
(+gβπ)π¦) β (π LMHom π)) |
15 | | simpr3 1197 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π§ β (π LMHom π)) |
16 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’ (((π₯ βf
(+gβπ)π¦) β (π LMHom π) β§ π§ β (π LMHom π)) β ((π₯ βf
(+gβπ)π¦)(+gβπ΄)π§) = ((π₯ βf
(+gβπ)π¦) βf
(+gβπ)π§)) |
17 | 14, 15, 16 | syl2anc 585 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ βf
(+gβπ)π¦)(+gβπ΄)π§) = ((π₯ βf
(+gβπ)π¦) βf
(+gβπ)π§)) |
18 | 12, 13, 8 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(+gβπ΄)π¦) = (π₯ βf
(+gβπ)π¦)) |
19 | 18 | oveq1d 7421 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(+gβπ΄)π¦)(+gβπ΄)π§) = ((π₯ βf
(+gβπ)π¦)(+gβπ΄)π§)) |
20 | 6 | lmhmplusg 20648 |
. . . . . . 7
β’ ((π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦ βf
(+gβπ)π§) β (π LMHom π)) |
21 | 13, 15, 20 | syl2anc 585 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦ βf
(+gβπ)π§) β (π LMHom π)) |
22 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . . 6
β’ ((π₯ β (π LMHom π) β§ (π¦ βf
(+gβπ)π§) β (π LMHom π)) β (π₯(+gβπ΄)(π¦ βf
(+gβπ)π§)) = (π₯ βf
(+gβπ)(π¦ βf
(+gβπ)π§))) |
23 | 12, 21, 22 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(+gβπ΄)(π¦ βf
(+gβπ)π§)) = (π₯ βf
(+gβπ)(π¦ βf
(+gβπ)π§))) |
24 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . . . 7
β’ ((π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦(+gβπ΄)π§) = (π¦ βf
(+gβπ)π§)) |
25 | 13, 15, 24 | syl2anc 585 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦(+gβπ΄)π§) = (π¦ βf
(+gβπ)π§)) |
26 | 25 | oveq2d 7422 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(+gβπ΄)(π¦(+gβπ΄)π§)) = (π₯(+gβπ΄)(π¦ βf
(+gβπ)π§))) |
27 | | lmodgrp 20471 |
. . . . . . . 8
β’ (π β LMod β π β Grp) |
28 | 27 | grpmndd 18829 |
. . . . . . 7
β’ (π β LMod β π β Mnd) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π β Mnd) |
30 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
31 | 30, 30 | lmhmf 20638 |
. . . . . . . 8
β’ (π₯ β (π LMHom π) β π₯:(Baseβπ)βΆ(Baseβπ)) |
32 | 12, 31 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯:(Baseβπ)βΆ(Baseβπ)) |
33 | | fvex 6902 |
. . . . . . . 8
β’
(Baseβπ)
β V |
34 | 33, 33 | elmap 8862 |
. . . . . . 7
β’ (π₯ β ((Baseβπ) βm
(Baseβπ)) β
π₯:(Baseβπ)βΆ(Baseβπ)) |
35 | 32, 34 | sylibr 233 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯ β ((Baseβπ) βm (Baseβπ))) |
36 | 30, 30 | lmhmf 20638 |
. . . . . . . 8
β’ (π¦ β (π LMHom π) β π¦:(Baseβπ)βΆ(Baseβπ)) |
37 | 13, 36 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦:(Baseβπ)βΆ(Baseβπ)) |
38 | 33, 33 | elmap 8862 |
. . . . . . 7
β’ (π¦ β ((Baseβπ) βm
(Baseβπ)) β
π¦:(Baseβπ)βΆ(Baseβπ)) |
39 | 37, 38 | sylibr 233 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦ β ((Baseβπ) βm (Baseβπ))) |
40 | 30, 30 | lmhmf 20638 |
. . . . . . . 8
β’ (π§ β (π LMHom π) β π§:(Baseβπ)βΆ(Baseβπ)) |
41 | 15, 40 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π§:(Baseβπ)βΆ(Baseβπ)) |
42 | 33, 33 | elmap 8862 |
. . . . . . 7
β’ (π§ β ((Baseβπ) βm
(Baseβπ)) β
π§:(Baseβπ)βΆ(Baseβπ)) |
43 | 41, 42 | sylibr 233 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π§ β ((Baseβπ) βm (Baseβπ))) |
44 | 30, 6 | mndvass 21886 |
. . . . . 6
β’ ((π β Mnd β§ (π₯ β ((Baseβπ) βm
(Baseβπ)) β§ π¦ β ((Baseβπ) βm
(Baseβπ)) β§ π§ β ((Baseβπ) βm
(Baseβπ)))) β
((π₯ βf
(+gβπ)π¦) βf
(+gβπ)π§) = (π₯ βf
(+gβπ)(π¦ βf
(+gβπ)π§))) |
45 | 29, 35, 39, 43, 44 | syl13anc 1373 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ βf
(+gβπ)π¦) βf
(+gβπ)π§) = (π₯ βf
(+gβπ)(π¦ βf
(+gβπ)π§))) |
46 | 23, 26, 45 | 3eqtr4d 2783 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(+gβπ΄)(π¦(+gβπ΄)π§)) = ((π₯ βf
(+gβπ)π¦) βf
(+gβπ)π§)) |
47 | 17, 19, 46 | 3eqtr4d 2783 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(+gβπ΄)π¦)(+gβπ΄)π§) = (π₯(+gβπ΄)(π¦(+gβπ΄)π§))) |
48 | | id 22 |
. . . 4
β’ (π β LMod β π β LMod) |
49 | | eqidd 2734 |
. . . 4
β’ (π β LMod β
(Scalarβπ) =
(Scalarβπ)) |
50 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
51 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
52 | 50, 30, 51, 51 | 0lmhm 20644 |
. . . 4
β’ ((π β LMod β§ π β LMod β§
(Scalarβπ) =
(Scalarβπ)) β
((Baseβπ) Γ
{(0gβπ)})
β (π LMHom π)) |
53 | 48, 48, 49, 52 | syl3anc 1372 |
. . 3
β’ (π β LMod β
((Baseβπ) Γ
{(0gβπ)})
β (π LMHom π)) |
54 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’
((((Baseβπ)
Γ {(0gβπ)}) β (π LMHom π) β§ π₯ β (π LMHom π)) β (((Baseβπ) Γ {(0gβπ)})(+gβπ΄)π₯) = (((Baseβπ) Γ {(0gβπ)}) βf
(+gβπ)π₯)) |
55 | 53, 54 | sylan 581 |
. . . 4
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((Baseβπ) Γ {(0gβπ)})(+gβπ΄)π₯) = (((Baseβπ) Γ {(0gβπ)}) βf
(+gβπ)π₯)) |
56 | 31, 34 | sylibr 233 |
. . . . 5
β’ (π₯ β (π LMHom π) β π₯ β ((Baseβπ) βm (Baseβπ))) |
57 | 30, 6, 50 | mndvlid 21887 |
. . . . 5
β’ ((π β Mnd β§ π₯ β ((Baseβπ) βm
(Baseβπ))) β
(((Baseβπ) Γ
{(0gβπ)})
βf (+gβπ)π₯) = π₯) |
58 | 28, 56, 57 | syl2an 597 |
. . . 4
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((Baseβπ) Γ {(0gβπ)}) βf
(+gβπ)π₯) = π₯) |
59 | 55, 58 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((Baseβπ) Γ {(0gβπ)})(+gβπ΄)π₯) = π₯) |
60 | | eqid 2733 |
. . . . 5
β’
(invgβπ) = (invgβπ) |
61 | 60 | invlmhm 20646 |
. . . 4
β’ (π β LMod β
(invgβπ)
β (π LMHom π)) |
62 | | lmhmco 20647 |
. . . 4
β’
(((invgβπ) β (π LMHom π) β§ π₯ β (π LMHom π)) β ((invgβπ) β π₯) β (π LMHom π)) |
63 | 61, 62 | sylan 581 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β ((invgβπ) β π₯) β (π LMHom π)) |
64 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’
((((invgβπ) β π₯) β (π LMHom π) β§ π₯ β (π LMHom π)) β (((invgβπ) β π₯)(+gβπ΄)π₯) = (((invgβπ) β π₯) βf
(+gβπ)π₯)) |
65 | 63, 64 | sylancom 589 |
. . . 4
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((invgβπ) β π₯)(+gβπ΄)π₯) = (((invgβπ) β π₯) βf
(+gβπ)π₯)) |
66 | 30, 6, 60, 50 | grpvlinv 21889 |
. . . . 5
β’ ((π β Grp β§ π₯ β ((Baseβπ) βm
(Baseβπ))) β
(((invgβπ)
β π₯)
βf (+gβπ)π₯) = ((Baseβπ) Γ {(0gβπ)})) |
67 | 27, 56, 66 | syl2an 597 |
. . . 4
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((invgβπ) β π₯) βf
(+gβπ)π₯) = ((Baseβπ) Γ {(0gβπ)})) |
68 | 65, 67 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (((invgβπ) β π₯)(+gβπ΄)π₯) = ((Baseβπ) Γ {(0gβπ)})) |
69 | 3, 4, 11, 47, 53, 59, 63, 68 | isgrpd 18841 |
. 2
β’ (π β LMod β π΄ β Grp) |
70 | | eqid 2733 |
. . . . 5
β’
(.rβπ΄) = (.rβπ΄) |
71 | 1, 2, 70 | mendmulr 41916 |
. . . 4
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(.rβπ΄)π¦) = (π₯ β π¦)) |
72 | | lmhmco 20647 |
. . . 4
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯ β π¦) β (π LMHom π)) |
73 | 71, 72 | eqeltrd 2834 |
. . 3
β’ ((π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(.rβπ΄)π¦) β (π LMHom π)) |
74 | 73 | 3adant1 1131 |
. 2
β’ ((π β LMod β§ π₯ β (π LMHom π) β§ π¦ β (π LMHom π)) β (π₯(.rβπ΄)π¦) β (π LMHom π)) |
75 | | coass 6262 |
. . 3
β’ ((π₯ β π¦) β π§) = (π₯ β (π¦ β π§)) |
76 | 12, 13, 71 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)π¦) = (π₯ β π¦)) |
77 | 76 | oveq1d 7421 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π¦)(.rβπ΄)π§) = ((π₯ β π¦)(.rβπ΄)π§)) |
78 | 12, 13, 72 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯ β π¦) β (π LMHom π)) |
79 | 1, 2, 70 | mendmulr 41916 |
. . . . 5
β’ (((π₯ β π¦) β (π LMHom π) β§ π§ β (π LMHom π)) β ((π₯ β π¦)(.rβπ΄)π§) = ((π₯ β π¦) β π§)) |
80 | 78, 15, 79 | syl2anc 585 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ β π¦)(.rβπ΄)π§) = ((π₯ β π¦) β π§)) |
81 | 77, 80 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π¦)(.rβπ΄)π§) = ((π₯ β π¦) β π§)) |
82 | 1, 2, 70 | mendmulr 41916 |
. . . . . 6
β’ ((π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦(.rβπ΄)π§) = (π¦ β π§)) |
83 | 13, 15, 82 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦(.rβπ΄)π§) = (π¦ β π§)) |
84 | 83 | oveq2d 7422 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦(.rβπ΄)π§)) = (π₯(.rβπ΄)(π¦ β π§))) |
85 | | lmhmco 20647 |
. . . . . 6
β’ ((π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦ β π§) β (π LMHom π)) |
86 | 13, 15, 85 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦ β π§) β (π LMHom π)) |
87 | 1, 2, 70 | mendmulr 41916 |
. . . . 5
β’ ((π₯ β (π LMHom π) β§ (π¦ β π§) β (π LMHom π)) β (π₯(.rβπ΄)(π¦ β π§)) = (π₯ β (π¦ β π§))) |
88 | 12, 86, 87 | syl2anc 585 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦ β π§)) = (π₯ β (π¦ β π§))) |
89 | 84, 88 | eqtrd 2773 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦(.rβπ΄)π§)) = (π₯ β (π¦ β π§))) |
90 | 75, 81, 89 | 3eqtr4a 2799 |
. 2
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π¦)(.rβπ΄)π§) = (π₯(.rβπ΄)(π¦(.rβπ΄)π§))) |
91 | 1, 2, 70 | mendmulr 41916 |
. . . 4
β’ ((π₯ β (π LMHom π) β§ (π¦ βf
(+gβπ)π§) β (π LMHom π)) β (π₯(.rβπ΄)(π¦ βf
(+gβπ)π§)) = (π₯ β (π¦ βf
(+gβπ)π§))) |
92 | 12, 21, 91 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦ βf
(+gβπ)π§)) = (π₯ β (π¦ βf
(+gβπ)π§))) |
93 | 25 | oveq2d 7422 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦(+gβπ΄)π§)) = (π₯(.rβπ΄)(π¦ βf
(+gβπ)π§))) |
94 | | lmhmco 20647 |
. . . . . 6
β’ ((π₯ β (π LMHom π) β§ π§ β (π LMHom π)) β (π₯ β π§) β (π LMHom π)) |
95 | 12, 15, 94 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯ β π§) β (π LMHom π)) |
96 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’ (((π₯ β π¦) β (π LMHom π) β§ (π₯ β π§) β (π LMHom π)) β ((π₯ β π¦)(+gβπ΄)(π₯ β π§)) = ((π₯ β π¦) βf
(+gβπ)(π₯ β π§))) |
97 | 78, 95, 96 | syl2anc 585 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ β π¦)(+gβπ΄)(π₯ β π§)) = ((π₯ β π¦) βf
(+gβπ)(π₯ β π§))) |
98 | 1, 2, 70 | mendmulr 41916 |
. . . . . 6
β’ ((π₯ β (π LMHom π) β§ π§ β (π LMHom π)) β (π₯(.rβπ΄)π§) = (π₯ β π§)) |
99 | 12, 15, 98 | syl2anc 585 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)π§) = (π₯ β π§)) |
100 | 76, 99 | oveq12d 7424 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π¦)(+gβπ΄)(π₯(.rβπ΄)π§)) = ((π₯ β π¦)(+gβπ΄)(π₯ β π§))) |
101 | | lmghm 20635 |
. . . . . 6
β’ (π₯ β (π LMHom π) β π₯ β (π GrpHom π)) |
102 | | ghmmhm 19097 |
. . . . . 6
β’ (π₯ β (π GrpHom π) β π₯ β (π MndHom π)) |
103 | 12, 101, 102 | 3syl 18 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯ β (π MndHom π)) |
104 | 30, 6, 6 | mhmvlin 21891 |
. . . . 5
β’ ((π₯ β (π MndHom π) β§ π¦ β ((Baseβπ) βm (Baseβπ)) β§ π§ β ((Baseβπ) βm (Baseβπ))) β (π₯ β (π¦ βf
(+gβπ)π§)) = ((π₯ β π¦) βf
(+gβπ)(π₯ β π§))) |
105 | 103, 39, 43, 104 | syl3anc 1372 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯ β (π¦ βf
(+gβπ)π§)) = ((π₯ β π¦) βf
(+gβπ)(π₯ β π§))) |
106 | 97, 100, 105 | 3eqtr4d 2783 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π¦)(+gβπ΄)(π₯(.rβπ΄)π§)) = (π₯ β (π¦ βf
(+gβπ)π§))) |
107 | 92, 93, 106 | 3eqtr4d 2783 |
. 2
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯(.rβπ΄)(π¦(+gβπ΄)π§)) = ((π₯(.rβπ΄)π¦)(+gβπ΄)(π₯(.rβπ΄)π§))) |
108 | 1, 2, 70 | mendmulr 41916 |
. . . 4
β’ (((π₯ βf
(+gβπ)π¦) β (π LMHom π) β§ π§ β (π LMHom π)) β ((π₯ βf
(+gβπ)π¦)(.rβπ΄)π§) = ((π₯ βf
(+gβπ)π¦) β π§)) |
109 | 14, 15, 108 | syl2anc 585 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ βf
(+gβπ)π¦)(.rβπ΄)π§) = ((π₯ βf
(+gβπ)π¦) β π§)) |
110 | 18 | oveq1d 7421 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(+gβπ΄)π¦)(.rβπ΄)π§) = ((π₯ βf
(+gβπ)π¦)(.rβπ΄)π§)) |
111 | 1, 2, 6, 7 | mendplusg 41914 |
. . . . 5
β’ (((π₯ β π§) β (π LMHom π) β§ (π¦ β π§) β (π LMHom π)) β ((π₯ β π§)(+gβπ΄)(π¦ β π§)) = ((π₯ β π§) βf
(+gβπ)(π¦ β π§))) |
112 | 95, 86, 111 | syl2anc 585 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ β π§)(+gβπ΄)(π¦ β π§)) = ((π₯ β π§) βf
(+gβπ)(π¦ β π§))) |
113 | 99, 83 | oveq12d 7424 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π§)(+gβπ΄)(π¦(.rβπ΄)π§)) = ((π₯ β π§)(+gβπ΄)(π¦ β π§))) |
114 | | ffn 6715 |
. . . . . 6
β’ (π₯:(Baseβπ)βΆ(Baseβπ) β π₯ Fn (Baseβπ)) |
115 | 12, 31, 114 | 3syl 18 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯ Fn (Baseβπ)) |
116 | | ffn 6715 |
. . . . . 6
β’ (π¦:(Baseβπ)βΆ(Baseβπ) β π¦ Fn (Baseβπ)) |
117 | 13, 36, 116 | 3syl 18 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦ Fn (Baseβπ)) |
118 | 33 | a1i 11 |
. . . . 5
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (Baseβπ) β V) |
119 | | inidm 4218 |
. . . . 5
β’
((Baseβπ)
β© (Baseβπ)) =
(Baseβπ) |
120 | 115, 117,
41, 118, 118, 118, 119 | ofco 7690 |
. . . 4
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯ βf
(+gβπ)π¦) β π§) = ((π₯ β π§) βf
(+gβπ)(π¦ β π§))) |
121 | 112, 113,
120 | 3eqtr4d 2783 |
. . 3
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(.rβπ΄)π§)(+gβπ΄)(π¦(.rβπ΄)π§)) = ((π₯ βf
(+gβπ)π¦) β π§)) |
122 | 109, 110,
121 | 3eqtr4d 2783 |
. 2
β’ ((π β LMod β§ (π₯ β (π LMHom π) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯(+gβπ΄)π¦)(.rβπ΄)π§) = ((π₯(.rβπ΄)π§)(+gβπ΄)(π¦(.rβπ΄)π§))) |
123 | 30 | idlmhm 20645 |
. 2
β’ (π β LMod β ( I βΎ
(Baseβπ)) β
(π LMHom π)) |
124 | 1, 2, 70 | mendmulr 41916 |
. . . 4
β’ ((( I
βΎ (Baseβπ))
β (π LMHom π) β§ π₯ β (π LMHom π)) β (( I βΎ (Baseβπ))(.rβπ΄)π₯) = (( I βΎ (Baseβπ)) β π₯)) |
125 | 123, 124 | sylan 581 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (( I βΎ (Baseβπ))(.rβπ΄)π₯) = (( I βΎ (Baseβπ)) β π₯)) |
126 | 31 | adantl 483 |
. . . 4
β’ ((π β LMod β§ π₯ β (π LMHom π)) β π₯:(Baseβπ)βΆ(Baseβπ)) |
127 | | fcoi2 6764 |
. . . 4
β’ (π₯:(Baseβπ)βΆ(Baseβπ) β (( I βΎ (Baseβπ)) β π₯) = π₯) |
128 | 126, 127 | syl 17 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (( I βΎ (Baseβπ)) β π₯) = π₯) |
129 | 125, 128 | eqtrd 2773 |
. 2
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (( I βΎ (Baseβπ))(.rβπ΄)π₯) = π₯) |
130 | | id 22 |
. . . 4
β’ (π₯ β (π LMHom π) β π₯ β (π LMHom π)) |
131 | 1, 2, 70 | mendmulr 41916 |
. . . 4
β’ ((π₯ β (π LMHom π) β§ ( I βΎ (Baseβπ)) β (π LMHom π)) β (π₯(.rβπ΄)( I βΎ (Baseβπ))) = (π₯ β ( I βΎ (Baseβπ)))) |
132 | 130, 123,
131 | syl2anr 598 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (π₯(.rβπ΄)( I βΎ (Baseβπ))) = (π₯ β ( I βΎ (Baseβπ)))) |
133 | | fcoi1 6763 |
. . . 4
β’ (π₯:(Baseβπ)βΆ(Baseβπ) β (π₯ β ( I βΎ (Baseβπ))) = π₯) |
134 | 126, 133 | syl 17 |
. . 3
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (π₯ β ( I βΎ (Baseβπ))) = π₯) |
135 | 132, 134 | eqtrd 2773 |
. 2
β’ ((π β LMod β§ π₯ β (π LMHom π)) β (π₯(.rβπ΄)( I βΎ (Baseβπ))) = π₯) |
136 | 3, 4, 5, 69, 74, 90, 107, 122, 123, 129, 135 | isringd 20099 |
1
β’ (π β LMod β π΄ β Ring) |