Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = 0 β (π₯ β π) = (0 β π)) |
2 | 1 | oveq2d 7378 |
. . . . . . . 8
β’ (π₯ = 0 β (π
Β· (π₯ β π)) = (π
Β· (0 β π))) |
3 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = 0 β (π₯πΈπ
) = (0πΈπ
)) |
4 | 3 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ = 0 β ((π₯πΈπ
) Β· π) = ((0πΈπ
) Β· π)) |
5 | 2, 4 | eqeq12d 2753 |
. . . . . . 7
β’ (π₯ = 0 β ((π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π) β (π
Β· (0 β π)) = ((0πΈπ
) Β· π))) |
6 | 5 | imbi2d 341 |
. . . . . 6
β’ (π₯ = 0 β ((((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π)) β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (0 β π)) = ((0πΈπ
) Β· π)))) |
7 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β π) = (π¦ β π)) |
8 | 7 | oveq2d 7378 |
. . . . . . . 8
β’ (π₯ = π¦ β (π
Β· (π₯ β π)) = (π
Β· (π¦ β π))) |
9 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯πΈπ
) = (π¦πΈπ
)) |
10 | 9 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π₯πΈπ
) Β· π) = ((π¦πΈπ
) Β· π)) |
11 | 8, 10 | eqeq12d 2753 |
. . . . . . 7
β’ (π₯ = π¦ β ((π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π) β (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π))) |
12 | 11 | imbi2d 341 |
. . . . . 6
β’ (π₯ = π¦ β ((((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π)) β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π)))) |
13 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = (π¦ + 1) β (π₯ β π) = ((π¦ + 1) β π)) |
14 | 13 | oveq2d 7378 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (π
Β· (π₯ β π)) = (π
Β· ((π¦ + 1) β π))) |
15 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = (π¦ + 1) β (π₯πΈπ
) = ((π¦ + 1)πΈπ
)) |
16 | 15 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β ((π₯πΈπ
) Β· π) = (((π¦ + 1)πΈπ
) Β· π)) |
17 | 14, 16 | eqeq12d 2753 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β ((π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π) β (π
Β· ((π¦ + 1) β π)) = (((π¦ + 1)πΈπ
) Β· π))) |
18 | 17 | imbi2d 341 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β ((((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π)) β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· ((π¦ + 1) β π)) = (((π¦ + 1)πΈπ
) Β· π)))) |
19 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β π) = (π β π)) |
20 | 19 | oveq2d 7378 |
. . . . . . . 8
β’ (π₯ = π β (π
Β· (π₯ β π)) = (π
Β· (π β π))) |
21 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = π β (π₯πΈπ
) = (ππΈπ
)) |
22 | 21 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ = π β ((π₯πΈπ
) Β· π) = ((ππΈπ
) Β· π)) |
23 | 20, 22 | eqeq12d 2753 |
. . . . . . 7
β’ (π₯ = π β ((π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π) β (π
Β· (π β π)) = ((ππΈπ
) Β· π))) |
24 | 23 | imbi2d 341 |
. . . . . 6
β’ (π₯ = π β ((((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π₯ β π)) = ((π₯πΈπ
) Β· π)) β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π β π)) = ((ππΈπ
) Β· π)))) |
25 | | simpr 486 |
. . . . . . . . . 10
β’ ((π
β πΎ β§ π β π) β π β π) |
26 | 25 | adantr 482 |
. . . . . . . . 9
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β π β π) |
27 | | lmodvsmdi.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
28 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
29 | | lmodvsmdi.p |
. . . . . . . . . 10
β’ β =
(.gβπ) |
30 | 27, 28, 29 | mulg0 18886 |
. . . . . . . . 9
β’ (π β π β (0 β π) = (0gβπ)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (0 β π) = (0gβπ)) |
32 | 31 | oveq2d 7378 |
. . . . . . 7
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (0 β π)) = (π
Β·
(0gβπ))) |
33 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π
β πΎ β§ π β π) β π
β πΎ) |
34 | 33 | anim1i 616 |
. . . . . . . . . 10
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π
β πΎ β§ π β LMod)) |
35 | 34 | ancomd 463 |
. . . . . . . . 9
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π β LMod β§ π
β πΎ)) |
36 | | lmodvsmdi.f |
. . . . . . . . . 10
β’ πΉ = (Scalarβπ) |
37 | | lmodvsmdi.s |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
38 | | lmodvsmdi.k |
. . . . . . . . . 10
β’ πΎ = (BaseβπΉ) |
39 | 36, 37, 38, 28 | lmodvs0 20372 |
. . . . . . . . 9
β’ ((π β LMod β§ π
β πΎ) β (π
Β·
(0gβπ)) =
(0gβπ)) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β·
(0gβπ)) =
(0gβπ)) |
41 | 25 | anim1i 616 |
. . . . . . . . . 10
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π β π β§ π β LMod)) |
42 | 41 | ancomd 463 |
. . . . . . . . 9
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π β LMod β§ π β π)) |
43 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβπΉ) = (0gβπΉ) |
44 | 27, 36, 37, 43, 28 | lmod0vs 20371 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β ((0gβπΉ) Β· π) = (0gβπ)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β
((0gβπΉ)
Β·
π) =
(0gβπ)) |
46 | 33 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β π
β πΎ) |
47 | | lmodvsmdi.e |
. . . . . . . . . . . 12
β’ πΈ = (.gβπΉ) |
48 | 38, 43, 47 | mulg0 18886 |
. . . . . . . . . . 11
β’ (π
β πΎ β (0πΈπ
) = (0gβπΉ)) |
49 | 48 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π
β πΎ β (0gβπΉ) = (0πΈπ
)) |
50 | 46, 49 | syl 17 |
. . . . . . . . 9
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β
(0gβπΉ) =
(0πΈπ
)) |
51 | 50 | oveq1d 7377 |
. . . . . . . 8
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β
((0gβπΉ)
Β·
π) = ((0πΈπ
) Β· π)) |
52 | 40, 45, 51 | 3eqtr2d 2783 |
. . . . . . 7
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β·
(0gβπ)) =
((0πΈπ
) Β· π)) |
53 | 32, 52 | eqtrd 2777 |
. . . . . 6
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (0 β π)) = ((0πΈπ
) Β· π)) |
54 | | lmodgrp 20345 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β π β Grp) |
55 | 54 | grpmndd 18767 |
. . . . . . . . . . . . . 14
β’ (π β LMod β π β Mnd) |
56 | 55 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β π β Mnd) |
57 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β π¦ β β0) |
58 | 26 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β π β π) |
59 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(+gβπ) = (+gβπ) |
60 | 27, 29, 59 | mulgnn0p1 18894 |
. . . . . . . . . . . . 13
β’ ((π β Mnd β§ π¦ β β0
β§ π β π) β ((π¦ + 1) β π) = ((π¦ β π)(+gβπ)π)) |
61 | 56, 57, 58, 60 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β ((π¦ + 1) β π) = ((π¦ β π)(+gβπ)π)) |
62 | 61 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (π
Β· ((π¦ + 1) β π)) = (π
Β· ((π¦ β π)(+gβπ)π))) |
63 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π
β πΎ β§ π β π) β§ π β LMod) β π β LMod) |
64 | 63 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β π β LMod) |
65 | | simprll 778 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β π
β πΎ) |
66 | 27, 29, 56, 57, 58 | mulgnn0cld 18904 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (π¦ β π) β π) |
67 | 27, 59, 36, 37, 38 | lmodvsdi 20361 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (π
β πΎ β§ (π¦ β π) β π β§ π β π)) β (π
Β· ((π¦ β π)(+gβπ)π)) = ((π
Β· (π¦ β π))(+gβπ)(π
Β· π))) |
68 | 64, 65, 66, 58, 67 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (π
Β· ((π¦ β π)(+gβπ)π)) = ((π
Β· (π¦ β π))(+gβπ)(π
Β· π))) |
69 | 62, 68 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (π
Β· ((π¦ + 1) β π)) = ((π
Β· (π¦ β π))(+gβπ)(π
Β· π))) |
70 | | oveq1 7369 |
. . . . . . . . . 10
β’ ((π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π) β ((π
Β· (π¦ β π))(+gβπ)(π
Β· π)) = (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π))) |
71 | 69, 70 | sylan9eq 2797 |
. . . . . . . . 9
β’ (((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β§ (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π)) β (π
Β· ((π¦ + 1) β π)) = (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π))) |
72 | 36 | lmodfgrp 20347 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β πΉ β Grp) |
73 | 72 | grpmndd 18767 |
. . . . . . . . . . . . . 14
β’ (π β LMod β πΉ β Mnd) |
74 | 73 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β πΉ β Mnd) |
75 | 38, 47, 74, 57, 65 | mulgnn0cld 18904 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (π¦πΈπ
) β πΎ) |
76 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(+gβπΉ) = (+gβπΉ) |
77 | 27, 59, 36, 37, 38, 76 | lmodvsdir 20362 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ ((π¦πΈπ
) β πΎ β§ π
β πΎ β§ π β π)) β (((π¦πΈπ
)(+gβπΉ)π
) Β· π) = (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π))) |
78 | 64, 75, 65, 58, 77 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπ
)(+gβπΉ)π
) Β· π) = (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π))) |
79 | 38, 47, 76 | mulgnn0p1 18894 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Mnd β§ π¦ β β0
β§ π
β πΎ) β ((π¦ + 1)πΈπ
) = ((π¦πΈπ
)(+gβπΉ)π
)) |
80 | 74, 57, 65, 79 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β ((π¦ + 1)πΈπ
) = ((π¦πΈπ
)(+gβπΉ)π
)) |
81 | 80 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β ((π¦πΈπ
)(+gβπΉ)π
) = ((π¦ + 1)πΈπ
)) |
82 | 81 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπ
)(+gβπΉ)π
) Β· π) = (((π¦ + 1)πΈπ
) Β· π)) |
83 | 78, 82 | eqtr3d 2779 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π)) = (((π¦ + 1)πΈπ
) Β· π)) |
84 | 83 | adantr 482 |
. . . . . . . . 9
β’ (((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β§ (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π)) β (((π¦πΈπ
) Β· π)(+gβπ)(π
Β· π)) = (((π¦ + 1)πΈπ
) Β· π)) |
85 | 71, 84 | eqtrd 2777 |
. . . . . . . 8
β’ (((π¦ β β0
β§ ((π
β πΎ β§ π β π) β§ π β LMod)) β§ (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π)) β (π
Β· ((π¦ + 1) β π)) = (((π¦ + 1)πΈπ
) Β· π)) |
86 | 85 | exp31 421 |
. . . . . . 7
β’ (π¦ β β0
β (((π
β πΎ β§ π β π) β§ π β LMod) β ((π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π) β (π
Β· ((π¦ + 1) β π)) = (((π¦ + 1)πΈπ
) Β· π)))) |
87 | 86 | a2d 29 |
. . . . . 6
β’ (π¦ β β0
β ((((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π¦ β π)) = ((π¦πΈπ
) Β· π)) β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· ((π¦ + 1) β π)) = (((π¦ + 1)πΈπ
) Β· π)))) |
88 | 6, 12, 18, 24, 53, 87 | nn0ind 12605 |
. . . . 5
β’ (π β β0
β (((π
β πΎ β§ π β π) β§ π β LMod) β (π
Β· (π β π)) = ((ππΈπ
) Β· π))) |
89 | 88 | exp4c 434 |
. . . 4
β’ (π β β0
β (π
β πΎ β (π β π β (π β LMod β (π
Β· (π β π)) = ((ππΈπ
) Β· π))))) |
90 | 89 | com12 32 |
. . 3
β’ (π
β πΎ β (π β β0 β (π β π β (π β LMod β (π
Β· (π β π)) = ((ππΈπ
) Β· π))))) |
91 | 90 | 3imp 1112 |
. 2
β’ ((π
β πΎ β§ π β β0 β§ π β π) β (π β LMod β (π
Β· (π β π)) = ((ππΈπ
) Β· π))) |
92 | 91 | impcom 409 |
1
β’ ((π β LMod β§ (π
β πΎ β§ π β β0 β§ π β π)) β (π
Β· (π β π)) = ((ππΈπ
) Β· π)) |