Step | Hyp | Ref
| Expression |
1 | | islmhm2.b |
. . . . 5
β’ π΅ = (Baseβπ) |
2 | | islmhm2.c |
. . . . 5
β’ πΆ = (Baseβπ) |
3 | 1, 2 | lmhmf 20510 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ:π΅βΆπΆ) |
4 | | islmhm2.k |
. . . . 5
β’ πΎ = (Scalarβπ) |
5 | | islmhm2.l |
. . . . 5
β’ πΏ = (Scalarβπ) |
6 | 4, 5 | lmhmsca 20506 |
. . . 4
β’ (πΉ β (π LMHom π) β πΏ = πΎ) |
7 | | lmghm 20507 |
. . . . . . . 8
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β πΉ β (π GrpHom π)) |
9 | | lmhmlmod1 20509 |
. . . . . . . . 9
β’ (πΉ β (π LMHom π) β π β LMod) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β π β LMod) |
11 | | simpr1 1195 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β π₯ β πΈ) |
12 | | simpr2 1196 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
13 | | islmhm2.m |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
14 | | islmhm2.e |
. . . . . . . . 9
β’ πΈ = (BaseβπΎ) |
15 | 1, 4, 13, 14 | lmodvscl 20354 |
. . . . . . . 8
β’ ((π β LMod β§ π₯ β πΈ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅) |
16 | 10, 11, 12, 15 | syl3anc 1372 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· π¦) β π΅) |
17 | | simpr3 1197 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β π§ β π΅) |
18 | | islmhm2.p |
. . . . . . . 8
β’ + =
(+gβπ) |
19 | | islmhm2.q |
. . . . . . . 8
⒠⨣ =
(+gβπ) |
20 | 1, 18, 19 | ghmlin 19018 |
. . . . . . 7
β’ ((πΉ β (π GrpHom π) β§ (π₯ Β· π¦) β π΅ β§ π§ β π΅) β (πΉβ((π₯ Β· π¦) + π§)) = ((πΉβ(π₯ Β· π¦)) ⨣ (πΉβπ§))) |
21 | 8, 16, 17, 20 | syl3anc 1372 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β (πΉβ((π₯ Β· π¦) + π§)) = ((πΉβ(π₯ Β· π¦)) ⨣ (πΉβπ§))) |
22 | | islmhm2.n |
. . . . . . . . 9
β’ Γ = (
Β·π βπ) |
23 | 4, 14, 1, 13, 22 | lmhmlin 20511 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ π₯ β πΈ β§ π¦ β π΅) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) |
24 | 23 | 3adant3r3 1185 |
. . . . . . 7
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) |
25 | 24 | oveq1d 7373 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β ((πΉβ(π₯ Β· π¦)) ⨣ (πΉβπ§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))) |
26 | 21, 25 | eqtrd 2773 |
. . . . 5
β’ ((πΉ β (π LMHom π) β§ (π₯ β πΈ β§ π¦ β π΅ β§ π§ β π΅)) β (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))) |
27 | 26 | ralrimivvva 3197 |
. . . 4
β’ (πΉ β (π LMHom π) β βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))) |
28 | 3, 6, 27 | 3jca 1129 |
. . 3
β’ (πΉ β (π LMHom π) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
29 | 28 | adantl 483 |
. 2
β’ (((π β LMod β§ π β LMod) β§ πΉ β (π LMHom π)) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
30 | | lmodgrp 20343 |
. . . . . 6
β’ (π β LMod β π β Grp) |
31 | | lmodgrp 20343 |
. . . . . 6
β’ (π β LMod β π β Grp) |
32 | 30, 31 | anim12i 614 |
. . . . 5
β’ ((π β LMod β§ π β LMod) β (π β Grp β§ π β Grp)) |
33 | 32 | adantr 482 |
. . . 4
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β (π β Grp β§ π β Grp)) |
34 | | simpr1 1195 |
. . . . 5
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β πΉ:π΅βΆπΆ) |
35 | 4 | lmodring 20344 |
. . . . . . . . . 10
β’ (π β LMod β πΎ β Ring) |
36 | 35 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β πΎ β Ring) |
37 | | eqid 2733 |
. . . . . . . . . 10
β’
(1rβπΎ) = (1rβπΎ) |
38 | 14, 37 | ringidcl 19994 |
. . . . . . . . 9
β’ (πΎ β Ring β
(1rβπΎ)
β πΈ) |
39 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π₯ = (1rβπΎ) β (π₯ Β· π¦) = ((1rβπΎ) Β· π¦)) |
40 | 39 | fvoveq1d 7380 |
. . . . . . . . . . . 12
β’ (π₯ = (1rβπΎ) β (πΉβ((π₯ Β· π¦) + π§)) = (πΉβ(((1rβπΎ) Β· π¦) + π§))) |
41 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π₯ = (1rβπΎ) β (π₯ Γ (πΉβπ¦)) = ((1rβπΎ) Γ (πΉβπ¦))) |
42 | 41 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π₯ = (1rβπΎ) β ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§))) |
43 | 40, 42 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π₯ = (1rβπΎ) β ((πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
44 | 43 | 2ralbidv 3209 |
. . . . . . . . . 10
β’ (π₯ = (1rβπΎ) β (βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
45 | 44 | rspcv 3576 |
. . . . . . . . 9
β’
((1rβπΎ) β πΈ β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
46 | 36, 38, 45 | 3syl 18 |
. . . . . . . 8
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) |
47 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β π β LMod) |
48 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
49 | 1, 4, 13, 37 | lmodvs1 20365 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π¦ β π΅) β ((1rβπΎ) Β· π¦) = π¦) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β ((1rβπΎ) Β· π¦) = π¦) |
51 | 50 | fvoveq1d 7380 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (πΉβ(π¦ + π§))) |
52 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β πΏ = πΎ) |
53 | 52 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β (1rβπΏ) = (1rβπΎ)) |
54 | 53 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β ((1rβπΏ) Γ (πΉβπ¦)) = ((1rβπΎ) Γ (πΉβπ¦))) |
55 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β π β LMod) |
56 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β πΉ:π΅βΆπΆ) |
57 | 56, 48 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β (πΉβπ¦) β πΆ) |
58 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(1rβπΏ) = (1rβπΏ) |
59 | 2, 5, 22, 58 | lmodvs1 20365 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ (πΉβπ¦) β πΆ) β ((1rβπΏ) Γ (πΉβπ¦)) = (πΉβπ¦)) |
60 | 55, 57, 59 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β ((1rβπΏ) Γ (πΉβπ¦)) = (πΉβπ¦)) |
61 | 54, 60 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β ((1rβπΎ) Γ (πΉβπ¦)) = (πΉβπ¦)) |
62 | 61 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)) = ((πΉβπ¦) ⨣ (πΉβπ§))) |
63 | 51, 62 | eqeq12d 2749 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β§ (π¦ β π΅ β§ π§ β π΅)) β ((πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§)))) |
64 | 63 | 2ralbidva 3207 |
. . . . . . . 8
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β (βπ¦ β π΅ βπ§ β π΅ (πΉβ(((1rβπΎ) Β· π¦) + π§)) = (((1rβπΎ) Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§)))) |
65 | 46, 64 | sylibd 238 |
. . . . . . 7
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ)) β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§)))) |
66 | 65 | exp32 422 |
. . . . . 6
β’ ((π β LMod β§ π β LMod) β (πΉ:π΅βΆπΆ β (πΏ = πΎ β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§)))))) |
67 | 66 | 3imp2 1350 |
. . . . 5
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§))) |
68 | 34, 67 | jca 513 |
. . . 4
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β (πΉ:π΅βΆπΆ β§ βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§)))) |
69 | 1, 2, 18, 19 | isghm 19013 |
. . . 4
β’ (πΉ β (π GrpHom π) β ((π β Grp β§ π β Grp) β§ (πΉ:π΅βΆπΆ β§ βπ¦ β π΅ βπ§ β π΅ (πΉβ(π¦ + π§)) = ((πΉβπ¦) ⨣ (πΉβπ§))))) |
70 | 33, 68, 69 | sylanbrc 584 |
. . 3
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β πΉ β (π GrpHom π)) |
71 | | simpr2 1196 |
. . 3
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β πΏ = πΎ) |
72 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
73 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
74 | 72, 73 | ghmid 19019 |
. . . . 5
β’ (πΉ β (π GrpHom π) β (πΉβ(0gβπ)) = (0gβπ)) |
75 | 70, 74 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β (πΉβ(0gβπ)) = (0gβπ)) |
76 | 30 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π β Grp) |
77 | 1, 72 | grpidcl 18783 |
. . . . . . . . . 10
β’ (π β Grp β
(0gβπ)
β π΅) |
78 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π§ = (0gβπ) β ((π₯ Β· π¦) + π§) = ((π₯ Β· π¦) + (0gβπ))) |
79 | 78 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π§ = (0gβπ) β (πΉβ((π₯ Β· π¦) + π§)) = (πΉβ((π₯ Β· π¦) + (0gβπ)))) |
80 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π§ = (0gβπ) β (πΉβπ§) = (πΉβ(0gβπ))) |
81 | 80 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π§ = (0gβπ) β ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ)))) |
82 | 79, 81 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π§ = (0gβπ) β ((πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ((π₯ Β· π¦) + (0gβπ))) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))))) |
83 | 82 | rspcv 3576 |
. . . . . . . . . 10
β’
((0gβπ) β π΅ β (βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ((π₯ Β· π¦) + (0gβπ))) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))))) |
84 | 76, 77, 83 | 3syl 18 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ((π₯ Β· π¦) + (0gβπ))) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))))) |
85 | | simplll 774 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π β LMod) |
86 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π₯ β πΈ) |
87 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π¦ β π΅) |
88 | 85, 86, 87, 15 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (π₯ Β· π¦) β π΅) |
89 | 1, 18, 72 | grprid 18786 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π₯ Β· π¦) β π΅) β ((π₯ Β· π¦) + (0gβπ)) = (π₯ Β· π¦)) |
90 | 76, 88, 89 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β ((π₯ Β· π¦) + (0gβπ)) = (π₯ Β· π¦)) |
91 | 90 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (πΉβ((π₯ Β· π¦) + (0gβπ))) = (πΉβ(π₯ Β· π¦))) |
92 | | simplr3 1218 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (πΉβ(0gβπ)) = (0gβπ)) |
93 | 92 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))) = ((π₯ Γ (πΉβπ¦)) ⨣
(0gβπ))) |
94 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π β LMod) |
95 | 94, 31 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π β Grp) |
96 | | simplr2 1217 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β πΏ = πΎ) |
97 | 96 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (BaseβπΏ) = (BaseβπΎ)) |
98 | 97, 14 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (BaseβπΏ) = πΈ) |
99 | 86, 98 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β π₯ β (BaseβπΏ)) |
100 | | simplr1 1216 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β πΉ:π΅βΆπΆ) |
101 | 100, 87 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (πΉβπ¦) β πΆ) |
102 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(BaseβπΏ) =
(BaseβπΏ) |
103 | 2, 5, 22, 102 | lmodvscl 20354 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π₯ β (BaseβπΏ) β§ (πΉβπ¦) β πΆ) β (π₯ Γ (πΉβπ¦)) β πΆ) |
104 | 94, 99, 101, 103 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (π₯ Γ (πΉβπ¦)) β πΆ) |
105 | 2, 19, 73 | grprid 18786 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π₯ Γ (πΉβπ¦)) β πΆ) β ((π₯ Γ (πΉβπ¦)) ⨣
(0gβπ)) =
(π₯ Γ (πΉβπ¦))) |
106 | 95, 104, 105 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β ((π₯ Γ (πΉβπ¦)) ⨣
(0gβπ)) =
(π₯ Γ (πΉβπ¦))) |
107 | 93, 106 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))) = (π₯ Γ (πΉβπ¦))) |
108 | 91, 107 | eqeq12d 2749 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β ((πΉβ((π₯ Β· π¦) + (0gβπ))) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβ(0gβπ))) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
109 | 84, 108 | sylibd 238 |
. . . . . . . 8
β’ ((((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β§ (π₯ β πΈ β§ π¦ β π΅)) β (βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
110 | 109 | ralimdvva 3198 |
. . . . . . 7
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ (πΉβ(0gβπ)) = (0gβπ))) β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
111 | 110 | 3exp2 1355 |
. . . . . 6
β’ ((π β LMod β§ π β LMod) β (πΉ:π΅βΆπΆ β (πΏ = πΎ β ((πΉβ(0gβπ)) = (0gβπ) β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))))) |
112 | 111 | com45 97 |
. . . . 5
β’ ((π β LMod β§ π β LMod) β (πΉ:π΅βΆπΆ β (πΏ = πΎ β (βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)) β ((πΉβ(0gβπ)) = (0gβπ) β βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))))) |
113 | 112 | 3imp2 1350 |
. . . 4
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β ((πΉβ(0gβπ)) = (0gβπ) β βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
114 | 75, 113 | mpd 15 |
. . 3
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) |
115 | 4, 5, 14, 1, 13, 22 | islmhm3 20504 |
. . . 4
β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
116 | 115 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
117 | 70, 71, 114, 116 | mpbir3and 1343 |
. 2
β’ (((π β LMod β§ π β LMod) β§ (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§)))) β πΉ β (π LMHom π)) |
118 | 29, 117 | impbida 800 |
1
β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ:π΅βΆπΆ β§ πΏ = πΎ β§ βπ₯ β πΈ βπ¦ β π΅ βπ§ β π΅ (πΉβ((π₯ Β· π¦) + π§)) = ((π₯ Γ (πΉβπ¦)) ⨣ (πΉβπ§))))) |