Step | Hyp | Ref
| Expression |
1 | | assaring 21283 |
. . . . . . . 8
β’ (π β AssAlg β π β Ring) |
2 | | assamulgscm.h |
. . . . . . . . 9
β’ π» = (mulGrpβπ) |
3 | 2 | ringmgp 19975 |
. . . . . . . 8
β’ (π β Ring β π» β Mnd) |
4 | 1, 3 | syl 17 |
. . . . . . 7
β’ (π β AssAlg β π» β Mnd) |
5 | 4 | adantl 483 |
. . . . . 6
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π» β Mnd) |
6 | 5 | adantl 483 |
. . . . 5
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π» β Mnd) |
7 | 6 | adantr 482 |
. . . 4
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β π» β Mnd) |
8 | | simpll 766 |
. . . 4
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β π¦ β β0) |
9 | | assalmod 21282 |
. . . . . . . 8
β’ (π β AssAlg β π β LMod) |
10 | 9 | adantl 483 |
. . . . . . 7
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π β LMod) |
11 | | simpll 766 |
. . . . . . 7
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π΄ β π΅) |
12 | | simplr 768 |
. . . . . . 7
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π β π) |
13 | | assamulgscm.v |
. . . . . . . 8
β’ π = (Baseβπ) |
14 | | assamulgscm.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
15 | | assamulgscm.s |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
16 | | assamulgscm.b |
. . . . . . . 8
β’ π΅ = (BaseβπΉ) |
17 | 13, 14, 15, 16 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π΄ β π΅ β§ π β π) β (π΄ Β· π) β π) |
18 | 10, 11, 12, 17 | syl3anc 1372 |
. . . . . 6
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π΄ Β· π) β π) |
19 | 18 | adantl 483 |
. . . . 5
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (π΄ Β· π) β π) |
20 | 19 | adantr 482 |
. . . 4
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β (π΄ Β· π) β π) |
21 | 2, 13 | mgpbas 19907 |
. . . . 5
β’ π = (Baseβπ») |
22 | | assamulgscm.e |
. . . . 5
β’ πΈ = (.gβπ») |
23 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
24 | 2, 23 | mgpplusg 19905 |
. . . . 5
β’
(.rβπ) = (+gβπ») |
25 | 21, 22, 24 | mulgnn0p1 18892 |
. . . 4
β’ ((π» β Mnd β§ π¦ β β0
β§ (π΄ Β· π) β π) β ((π¦ + 1)πΈ(π΄ Β· π)) = ((π¦πΈ(π΄ Β· π))(.rβπ)(π΄ Β· π))) |
26 | 7, 8, 20, 25 | syl3anc 1372 |
. . 3
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β ((π¦ + 1)πΈ(π΄ Β· π)) = ((π¦πΈ(π΄ Β· π))(.rβπ)(π΄ Β· π))) |
27 | | oveq1 7365 |
. . . 4
β’ ((π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)) β ((π¦πΈ(π΄ Β· π))(.rβπ)(π΄ Β· π)) = (((π¦ β π΄) Β· (π¦πΈπ))(.rβπ)(π΄ Β· π))) |
28 | | simprr 772 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π β AssAlg) |
29 | | assamulgscm.g |
. . . . . . . 8
β’ πΊ = (mulGrpβπΉ) |
30 | 14 | eqcomi 2742 |
. . . . . . . . 9
β’
(Scalarβπ) =
πΉ |
31 | 30 | fveq2i 6846 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (BaseβπΉ) |
32 | 29, 31 | mgpbas 19907 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (BaseβπΊ) |
33 | | assamulgscm.p |
. . . . . . 7
β’ β =
(.gβπΊ) |
34 | 14 | assasca 21284 |
. . . . . . . . . 10
β’ (π β AssAlg β πΉ β CRing) |
35 | | crngring 19981 |
. . . . . . . . . 10
β’ (πΉ β CRing β πΉ β Ring) |
36 | 29 | ringmgp 19975 |
. . . . . . . . . 10
β’ (πΉ β Ring β πΊ β Mnd) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . 9
β’ (π β AssAlg β πΊ β Mnd) |
38 | 37 | adantl 483 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β πΊ β Mnd) |
39 | 38 | adantl 483 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β πΊ β Mnd) |
40 | | simpl 484 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π¦ β β0) |
41 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β AssAlg β π΅ = (BaseβπΉ)) |
42 | 14 | fveq2i 6846 |
. . . . . . . . . . . . 13
β’
(BaseβπΉ) =
(Baseβ(Scalarβπ)) |
43 | 41, 42 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π β AssAlg β π΅ =
(Baseβ(Scalarβπ))) |
44 | 43 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π β AssAlg β (π΄ β π΅ β π΄ β (Baseβ(Scalarβπ)))) |
45 | 44 | biimpcd 249 |
. . . . . . . . . 10
β’ (π΄ β π΅ β (π β AssAlg β π΄ β (Baseβ(Scalarβπ)))) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β π΅ β§ π β π) β (π β AssAlg β π΄ β (Baseβ(Scalarβπ)))) |
47 | 46 | imp 408 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β π΄ β (Baseβ(Scalarβπ))) |
48 | 47 | adantl 483 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π΄ β (Baseβ(Scalarβπ))) |
49 | 32, 33, 39, 40, 48 | mulgnn0cld 18902 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (π¦ β π΄) β (Baseβ(Scalarβπ))) |
50 | | simprlr 779 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π β π) |
51 | 21, 22, 6, 40, 50 | mulgnn0cld 18902 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (π¦πΈπ) β π) |
52 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
53 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
54 | 13, 52, 53, 15, 23 | assaass 21280 |
. . . . . 6
β’ ((π β AssAlg β§ ((π¦ β π΄) β (Baseβ(Scalarβπ)) β§ (π¦πΈπ) β π β§ (π΄ Β· π) β π)) β (((π¦ β π΄) Β· (π¦πΈπ))(.rβπ)(π΄ Β· π)) = ((π¦ β π΄) Β· ((π¦πΈπ)(.rβπ)(π΄ Β· π)))) |
55 | 28, 49, 51, 19, 54 | syl13anc 1373 |
. . . . 5
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (((π¦ β π΄) Β· (π¦πΈπ))(.rβπ)(π΄ Β· π)) = ((π¦ β π΄) Β· ((π¦πΈπ)(.rβπ)(π΄ Β· π)))) |
56 | 13, 52, 53, 15, 23 | assaassr 21281 |
. . . . . . . 8
β’ ((π β AssAlg β§ (π΄ β
(Baseβ(Scalarβπ)) β§ (π¦πΈπ) β π β§ π β π)) β ((π¦πΈπ)(.rβπ)(π΄ Β· π)) = (π΄ Β· ((π¦πΈπ)(.rβπ)π))) |
57 | 28, 48, 51, 50, 56 | syl13anc 1373 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦πΈπ)(.rβπ)(π΄ Β· π)) = (π΄ Β· ((π¦πΈπ)(.rβπ)π))) |
58 | 57 | oveq2d 7374 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄) Β· ((π¦πΈπ)(.rβπ)(π΄ Β· π))) = ((π¦ β π΄) Β· (π΄ Β· ((π¦πΈπ)(.rβπ)π)))) |
59 | 21, 22, 24 | mulgnn0p1 18892 |
. . . . . . . . . 10
β’ ((π» β Mnd β§ π¦ β β0
β§ π β π) β ((π¦ + 1)πΈπ) = ((π¦πΈπ)(.rβπ)π)) |
60 | 6, 40, 50, 59 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ + 1)πΈπ) = ((π¦πΈπ)(.rβπ)π)) |
61 | 60 | eqcomd 2739 |
. . . . . . . 8
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦πΈπ)(.rβπ)π) = ((π¦ + 1)πΈπ)) |
62 | 61 | oveq2d 7374 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (π΄ Β· ((π¦πΈπ)(.rβπ)π)) = (π΄ Β· ((π¦ + 1)πΈπ))) |
63 | 62 | oveq2d 7374 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄) Β· (π΄ Β· ((π¦πΈπ)(.rβπ)π))) = ((π¦ β π΄) Β· (π΄ Β· ((π¦ + 1)πΈπ)))) |
64 | 10 | adantl 483 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π β LMod) |
65 | | peano2nn0 12458 |
. . . . . . . . 9
β’ (π¦ β β0
β (π¦ + 1) β
β0) |
66 | 65 | adantr 482 |
. . . . . . . 8
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (π¦ + 1) β
β0) |
67 | 21, 22, 6, 66, 50 | mulgnn0cld 18902 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ + 1)πΈπ) β π) |
68 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
69 | 13, 52, 15, 53, 68 | lmodvsass 20362 |
. . . . . . . 8
β’ ((π β LMod β§ ((π¦ β π΄) β (Baseβ(Scalarβπ)) β§ π΄ β (Baseβ(Scalarβπ)) β§ ((π¦ + 1)πΈπ) β π)) β (((π¦ β π΄)(.rβ(Scalarβπ))π΄) Β· ((π¦ + 1)πΈπ)) = ((π¦ β π΄) Β· (π΄ Β· ((π¦ + 1)πΈπ)))) |
70 | 69 | eqcomd 2739 |
. . . . . . 7
β’ ((π β LMod β§ ((π¦ β π΄) β (Baseβ(Scalarβπ)) β§ π΄ β (Baseβ(Scalarβπ)) β§ ((π¦ + 1)πΈπ) β π)) β ((π¦ β π΄) Β· (π΄ Β· ((π¦ + 1)πΈπ))) = (((π¦ β π΄)(.rβ(Scalarβπ))π΄) Β· ((π¦ + 1)πΈπ))) |
71 | 64, 49, 48, 67, 70 | syl13anc 1373 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄) Β· (π΄ Β· ((π¦ + 1)πΈπ))) = (((π¦ β π΄)(.rβ(Scalarβπ))π΄) Β· ((π¦ + 1)πΈπ))) |
72 | 58, 63, 71 | 3eqtrd 2777 |
. . . . 5
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄) Β· ((π¦πΈπ)(.rβπ)(π΄ Β· π))) = (((π¦ β π΄)(.rβ(Scalarβπ))π΄) Β· ((π¦ + 1)πΈπ))) |
73 | | simprll 778 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β π΄ β π΅) |
74 | 29, 16 | mgpbas 19907 |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
75 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.rβπΉ) = (.rβπΉ) |
76 | 29, 75 | mgpplusg 19905 |
. . . . . . . . . 10
β’
(.rβπΉ) = (+gβπΊ) |
77 | 74, 33, 76 | mulgnn0p1 18892 |
. . . . . . . . 9
β’ ((πΊ β Mnd β§ π¦ β β0
β§ π΄ β π΅) β ((π¦ + 1) β π΄) = ((π¦ β π΄)(.rβπΉ)π΄)) |
78 | 39, 40, 73, 77 | syl3anc 1372 |
. . . . . . . 8
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ + 1) β π΄) = ((π¦ β π΄)(.rβπΉ)π΄)) |
79 | 14 | a1i 11 |
. . . . . . . . . 10
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β πΉ = (Scalarβπ)) |
80 | 79 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β
(.rβπΉ) =
(.rβ(Scalarβπ))) |
81 | 80 | oveqd 7375 |
. . . . . . . 8
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄)(.rβπΉ)π΄) = ((π¦ β π΄)(.rβ(Scalarβπ))π΄)) |
82 | 78, 81 | eqtrd 2773 |
. . . . . . 7
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ + 1) β π΄) = ((π¦ β π΄)(.rβ(Scalarβπ))π΄)) |
83 | 82 | eqcomd 2739 |
. . . . . 6
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β ((π¦ β π΄)(.rβ(Scalarβπ))π΄) = ((π¦ + 1) β π΄)) |
84 | 83 | oveq1d 7373 |
. . . . 5
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (((π¦ β π΄)(.rβ(Scalarβπ))π΄) Β· ((π¦ + 1)πΈπ)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))) |
85 | 55, 72, 84 | 3eqtrd 2777 |
. . . 4
β’ ((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β (((π¦ β π΄) Β· (π¦πΈπ))(.rβπ)(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))) |
86 | 27, 85 | sylan9eqr 2795 |
. . 3
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β ((π¦πΈ(π΄ Β· π))(.rβπ)(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))) |
87 | 26, 86 | eqtrd 2773 |
. 2
β’ (((π¦ β β0
β§ ((π΄ β π΅ β§ π β π) β§ π β AssAlg)) β§ (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))) |
88 | 87 | exp31 421 |
1
β’ (π¦ β β0
β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) |