Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . . 7
β’ (π₯ = 0 β (π₯ β (πΆ Β· π)) = (0 β (πΆ Β· π))) |
2 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = 0 β (π₯πΈπΆ) = (0πΈπΆ)) |
3 | 2 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = 0 β ((π₯πΈπΆ) Β· π) = ((0πΈπΆ) Β· π)) |
4 | 1, 3 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = 0 β ((π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π) β (0 β (πΆ Β· π)) = ((0πΈπΆ) Β· π))) |
5 | 4 | imbi2d 341 |
. . . . 5
β’ (π₯ = 0 β ((((πΆ β πΎ β§ π β π) β§ π β LMod) β (π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π)) β (((πΆ β πΎ β§ π β π) β§ π β LMod) β (0 β (πΆ Β· π)) = ((0πΈπΆ) Β· π)))) |
6 | | oveq1 7369 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯ β (πΆ Β· π)) = (π¦ β (πΆ Β· π))) |
7 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯πΈπΆ) = (π¦πΈπΆ)) |
8 | 7 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = π¦ β ((π₯πΈπΆ) Β· π) = ((π¦πΈπΆ) Β· π)) |
9 | 6, 8 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = π¦ β ((π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π) β (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π))) |
10 | 9 | imbi2d 341 |
. . . . 5
β’ (π₯ = π¦ β ((((πΆ β πΎ β§ π β π) β§ π β LMod) β (π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π)) β (((πΆ β πΎ β§ π β π) β§ π β LMod) β (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π)))) |
11 | | oveq1 7369 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β (π₯ β (πΆ Β· π)) = ((π¦ + 1) β (πΆ Β· π))) |
12 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (π₯πΈπΆ) = ((π¦ + 1)πΈπΆ)) |
13 | 12 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β ((π₯πΈπΆ) Β· π) = (((π¦ + 1)πΈπΆ) Β· π)) |
14 | 11, 13 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β ((π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π) β ((π¦ + 1) β (πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π))) |
15 | 14 | imbi2d 341 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((((πΆ β πΎ β§ π β π) β§ π β LMod) β (π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π)) β (((πΆ β πΎ β§ π β π) β§ π β LMod) β ((π¦ + 1) β (πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)))) |
16 | | oveq1 7369 |
. . . . . . 7
β’ (π₯ = π β (π₯ β (πΆ Β· π)) = (π β (πΆ Β· π))) |
17 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = π β (π₯πΈπΆ) = (ππΈπΆ)) |
18 | 17 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = π β ((π₯πΈπΆ) Β· π) = ((ππΈπΆ) Β· π)) |
19 | 16, 18 | eqeq12d 2753 |
. . . . . 6
β’ (π₯ = π β ((π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π) β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π))) |
20 | 19 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β ((((πΆ β πΎ β§ π β π) β§ π β LMod) β (π₯ β (πΆ Β· π)) = ((π₯πΈπΆ) Β· π)) β (((πΆ β πΎ β§ π β π) β§ π β LMod) β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π)))) |
21 | | simpr 486 |
. . . . . . 7
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β π β LMod) |
22 | | simpr 486 |
. . . . . . . 8
β’ ((πΆ β πΎ β§ π β π) β π β π) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β π β π) |
24 | | lmodvsmmulgdi.v |
. . . . . . . 8
β’ π = (Baseβπ) |
25 | | lmodvsmmulgdi.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
26 | | lmodvsmmulgdi.s |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
27 | | eqid 2737 |
. . . . . . . 8
β’
(0gβπΉ) = (0gβπΉ) |
28 | | eqid 2737 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
29 | 24, 25, 26, 27, 28 | lmod0vs 20371 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β ((0gβπΉ) Β· π) = (0gβπ)) |
30 | 21, 23, 29 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β
((0gβπΉ)
Β·
π) =
(0gβπ)) |
31 | | simpl 484 |
. . . . . . . . 9
β’ ((πΆ β πΎ β§ π β π) β πΆ β πΎ) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β πΆ β πΎ) |
33 | | lmodvsmmulgdi.k |
. . . . . . . . 9
β’ πΎ = (BaseβπΉ) |
34 | | lmodvsmmulgdi.e |
. . . . . . . . 9
β’ πΈ = (.gβπΉ) |
35 | 33, 27, 34 | mulg0 18886 |
. . . . . . . 8
β’ (πΆ β πΎ β (0πΈπΆ) = (0gβπΉ)) |
36 | 32, 35 | syl 17 |
. . . . . . 7
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β (0πΈπΆ) = (0gβπΉ)) |
37 | 36 | oveq1d 7377 |
. . . . . 6
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β ((0πΈπΆ) Β· π) = ((0gβπΉ) Β· π)) |
38 | 24, 25, 26, 33 | lmodvscl 20355 |
. . . . . . . 8
β’ ((π β LMod β§ πΆ β πΎ β§ π β π) β (πΆ Β· π) β π) |
39 | 21, 32, 23, 38 | syl3anc 1372 |
. . . . . . 7
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β (πΆ Β· π) β π) |
40 | | lmodvsmmulgdi.p |
. . . . . . . 8
β’ β =
(.gβπ) |
41 | 24, 28, 40 | mulg0 18886 |
. . . . . . 7
β’ ((πΆ Β· π) β π β (0 β (πΆ Β· π)) = (0gβπ)) |
42 | 39, 41 | syl 17 |
. . . . . 6
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β (0 β (πΆ Β· π)) = (0gβπ)) |
43 | 30, 37, 42 | 3eqtr4rd 2788 |
. . . . 5
β’ (((πΆ β πΎ β§ π β π) β§ π β LMod) β (0 β (πΆ Β· π)) = ((0πΈπΆ) Β· π)) |
44 | | lmodgrp 20345 |
. . . . . . . . . . . 12
β’ (π β LMod β π β Grp) |
45 | 44 | grpmndd 18767 |
. . . . . . . . . . 11
β’ (π β LMod β π β Mnd) |
46 | 45 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β π β Mnd) |
47 | | simpl 484 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β π¦ β β0) |
48 | 39 | adantl 483 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β (πΆ Β· π) β π) |
49 | | eqid 2737 |
. . . . . . . . . . 11
β’
(+gβπ) = (+gβπ) |
50 | 24, 40, 49 | mulgnn0p1 18894 |
. . . . . . . . . 10
β’ ((π β Mnd β§ π¦ β β0
β§ (πΆ Β· π) β π) β ((π¦ + 1) β (πΆ Β· π)) = ((π¦ β (πΆ Β· π))(+gβπ)(πΆ Β· π))) |
51 | 46, 47, 48, 50 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β ((π¦ + 1) β (πΆ Β· π)) = ((π¦ β (πΆ Β· π))(+gβπ)(πΆ Β· π))) |
52 | 51 | adantr 482 |
. . . . . . . 8
β’ (((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β§ (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π)) β ((π¦ + 1) β (πΆ Β· π)) = ((π¦ β (πΆ Β· π))(+gβπ)(πΆ Β· π))) |
53 | | oveq1 7369 |
. . . . . . . . 9
β’ ((π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π) β ((π¦ β (πΆ Β· π))(+gβπ)(πΆ Β· π)) = (((π¦πΈπΆ) Β· π)(+gβπ)(πΆ Β· π))) |
54 | 21 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β π β LMod) |
55 | 25 | lmodring 20346 |
. . . . . . . . . . . . . 14
β’ (π β LMod β πΉ β Ring) |
56 | | ringmnd 19981 |
. . . . . . . . . . . . . 14
β’ (πΉ β Ring β πΉ β Mnd) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β LMod β πΉ β Mnd) |
58 | 57 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β πΉ β Mnd) |
59 | | simprll 778 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β πΆ β πΎ) |
60 | 33, 34, 58, 47, 59 | mulgnn0cld 18904 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β (π¦πΈπΆ) β πΎ) |
61 | 23 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β π β π) |
62 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(+gβπΉ) = (+gβπΉ) |
63 | 24, 49, 25, 26, 33, 62 | lmodvsdir 20362 |
. . . . . . . . . . 11
β’ ((π β LMod β§ ((π¦πΈπΆ) β πΎ β§ πΆ β πΎ β§ π β π)) β (((π¦πΈπΆ)(+gβπΉ)πΆ) Β· π) = (((π¦πΈπΆ) Β· π)(+gβπ)(πΆ Β· π))) |
64 | 54, 60, 59, 61, 63 | syl13anc 1373 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπΆ)(+gβπΉ)πΆ) Β· π) = (((π¦πΈπΆ) Β· π)(+gβπ)(πΆ Β· π))) |
65 | 33, 34, 62 | mulgnn0p1 18894 |
. . . . . . . . . . . . 13
β’ ((πΉ β Mnd β§ π¦ β β0
β§ πΆ β πΎ) β ((π¦ + 1)πΈπΆ) = ((π¦πΈπΆ)(+gβπΉ)πΆ)) |
66 | 58, 47, 59, 65 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β ((π¦ + 1)πΈπΆ) = ((π¦πΈπΆ)(+gβπΉ)πΆ)) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β ((π¦πΈπΆ)(+gβπΉ)πΆ) = ((π¦ + 1)πΈπΆ)) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπΆ)(+gβπΉ)πΆ) Β· π) = (((π¦ + 1)πΈπΆ) Β· π)) |
69 | 64, 68 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπΆ) Β· π)(+gβπ)(πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)) |
70 | 53, 69 | sylan9eqr 2799 |
. . . . . . . 8
β’ (((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β§ (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π)) β ((π¦ β (πΆ Β· π))(+gβπ)(πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)) |
71 | 52, 70 | eqtrd 2777 |
. . . . . . 7
β’ (((π¦ β β0
β§ ((πΆ β πΎ β§ π β π) β§ π β LMod)) β§ (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π)) β ((π¦ + 1) β (πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)) |
72 | 71 | exp31 421 |
. . . . . 6
β’ (π¦ β β0
β (((πΆ β πΎ β§ π β π) β§ π β LMod) β ((π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π) β ((π¦ + 1) β (πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)))) |
73 | 72 | a2d 29 |
. . . . 5
β’ (π¦ β β0
β ((((πΆ β πΎ β§ π β π) β§ π β LMod) β (π¦ β (πΆ Β· π)) = ((π¦πΈπΆ) Β· π)) β (((πΆ β πΎ β§ π β π) β§ π β LMod) β ((π¦ + 1) β (πΆ Β· π)) = (((π¦ + 1)πΈπΆ) Β· π)))) |
74 | 5, 10, 15, 20, 43, 73 | nn0ind 12605 |
. . . 4
β’ (π β β0
β (((πΆ β πΎ β§ π β π) β§ π β LMod) β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π))) |
75 | 74 | exp4c 434 |
. . 3
β’ (π β β0
β (πΆ β πΎ β (π β π β (π β LMod β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π))))) |
76 | 75 | 3imp21 1115 |
. 2
β’ ((πΆ β πΎ β§ π β β0 β§ π β π) β (π β LMod β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π))) |
77 | 76 | impcom 409 |
1
β’ ((π β LMod β§ (πΆ β πΎ β§ π β β0 β§ π β π)) β (π β (πΆ Β· π)) = ((ππΈπΆ) Β· π)) |