Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(1o mPoly π
) = (1o mPoly π
) |
2 | | psr1baslem 21572 |
. . 3
β’
(β0 βm 1o) = {π β (β0
βm 1o) β£ (β‘π β β) β
Fin} |
3 | | eqid 2733 |
. . 3
β’
(0gβπ
) = (0gβπ
) |
4 | | eqid 2733 |
. . 3
β’
(1rβπ
) = (1rβπ
) |
5 | | 1onn 8587 |
. . . 4
β’
1o β Ο |
6 | 5 | a1i 11 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β 1o β
Ο) |
7 | | ply1coe.p |
. . . 4
β’ π = (Poly1βπ
) |
8 | | eqid 2733 |
. . . 4
β’
(PwSer1βπ
) = (PwSer1βπ
) |
9 | | ply1coe.b |
. . . 4
β’ π΅ = (Baseβπ) |
10 | 7, 8, 9 | ply1bas 21582 |
. . 3
β’ π΅ = (Baseβ(1o
mPoly π
)) |
11 | | ply1coe.n |
. . . 4
β’ Β· = (
Β·π βπ) |
12 | 7, 1, 11 | ply1vsca 21613 |
. . 3
β’ Β· = (
Β·π β(1o mPoly π
)) |
13 | | simpl 484 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β π
β Ring) |
14 | | simpr 486 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β πΎ β π΅) |
15 | 1, 2, 3, 4, 6, 10,
12, 13, 14 | mplcoe1 21454 |
. 2
β’ ((π
β Ring β§ πΎ β π΅) β πΎ = ((1o mPoly π
) Ξ£g (π β (β0
βm 1o) β¦ ((πΎβπ) Β· (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
))))))) |
16 | | ply1coe.a |
. . . . . . 7
β’ π΄ = (coe1βπΎ) |
17 | 16 | fvcoe1 21594 |
. . . . . 6
β’ ((πΎ β π΅ β§ π β (β0
βm 1o)) β (πΎβπ) = (π΄β(πββ
))) |
18 | 17 | adantll 713 |
. . . . 5
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (πΎβπ) = (π΄β(πββ
))) |
19 | 5 | a1i 11 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β 1o β
Ο) |
20 | | eqid 2733 |
. . . . . . 7
β’
(mulGrpβ(1o mPoly π
)) = (mulGrpβ(1o mPoly
π
)) |
21 | | eqid 2733 |
. . . . . . 7
β’
(.gβ(mulGrpβ(1o mPoly π
))) =
(.gβ(mulGrpβ(1o mPoly π
))) |
22 | | eqid 2733 |
. . . . . . 7
β’
(1o mVar π
) = (1o mVar π
) |
23 | | simpll 766 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β π
β Ring) |
24 | | simpr 486 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β π β (β0
βm 1o)) |
25 | | eqidd 2734 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
)) = (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
))) |
26 | | 0ex 5265 |
. . . . . . . . . . 11
β’ β
β V |
27 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = β
β
((1o mVar π
)βπ) = ((1o mVar π
)ββ
)) |
28 | 27 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π = β
β
(((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
))) |
29 | 27 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = β
β
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
))) |
30 | 28, 29 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π = β
β
((((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ))
β (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
)) = (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
)))) |
31 | 26, 30 | ralsn 4643 |
. . . . . . . . . 10
β’
(βπ β
{β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ))
β (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
)) = (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)ββ
))) |
32 | 25, 31 | sylibr 233 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ))) |
33 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β
((1o mVar π
)βπ₯) = ((1o mVar π
)ββ
)) |
34 | 33 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π₯ = β
β
(((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
))) |
35 | 33 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π₯ = β
β
(((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) = (((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ))) |
36 | 34, 35 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π₯ = β
β
((((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) β (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ)))) |
37 | 36 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π₯ = β
β (βπ β {β
}
(((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) β βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ)))) |
38 | 26, 37 | ralsn 4643 |
. . . . . . . . 9
β’
(βπ₯ β
{β
}βπ β
{β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) β βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)ββ
)) =
(((1o mVar π
)ββ
)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar π
)βπ))) |
39 | 32, 38 | sylibr 233 |
. . . . . . . 8
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β βπ₯ β {β
}βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) |
40 | | df1o2 8420 |
. . . . . . . . 9
β’
1o = {β
} |
41 | 40 | raleqi 3310 |
. . . . . . . . 9
β’
(βπ β
1o (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) β βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) |
42 | 40, 41 | raleqbii 3314 |
. . . . . . . 8
β’
(βπ₯ β
1o βπ
β 1o (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) β βπ₯ β {β
}βπ β {β
} (((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) |
43 | 39, 42 | sylibr 233 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β βπ₯ β 1o βπ β 1o
(((1o mVar π
)βπ)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ₯)) = (((1o mVar π
)βπ₯)(+gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) |
44 | 1, 2, 3, 4, 19, 20, 21, 22, 23, 24, 43 | mplcoe5 21457 |
. . . . . 6
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
))) = ((mulGrpβ(1o mPoly
π
))
Ξ£g (π β 1o β¦ ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))))) |
45 | 40 | mpteq1i 5202 |
. . . . . . . 8
β’ (π β 1o β¦
((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) = (π β {β
} β¦ ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ))) |
46 | 45 | oveq2i 7369 |
. . . . . . 7
β’
((mulGrpβ(1o mPoly π
)) Ξ£g (π β 1o β¦
((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)))) = ((mulGrpβ(1o mPoly π
)) Ξ£g (π β {β
} β¦ ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)))) |
47 | 1 | mplring 21440 |
. . . . . . . . . . 11
β’
((1o β Ο β§ π
β Ring) β (1o mPoly
π
) β
Ring) |
48 | 5, 47 | mpan 689 |
. . . . . . . . . 10
β’ (π
β Ring β
(1o mPoly π
)
β Ring) |
49 | 20 | ringmgp 19975 |
. . . . . . . . . 10
β’
((1o mPoly π
) β Ring β
(mulGrpβ(1o mPoly π
)) β Mnd) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ (π
β Ring β
(mulGrpβ(1o mPoly π
)) β Mnd) |
51 | 50 | ad2antrr 725 |
. . . . . . . 8
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (mulGrpβ(1o mPoly
π
)) β
Mnd) |
52 | 26 | a1i 11 |
. . . . . . . 8
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β β
β V) |
53 | | ply1coe.e |
. . . . . . . . . . . 12
β’ β =
(.gβπ) |
54 | 20, 10 | mgpbas 19907 |
. . . . . . . . . . . . 13
β’ π΅ =
(Baseβ(mulGrpβ(1o mPoly π
))) |
55 | 54 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΎ β π΅) β π΅ = (Baseβ(mulGrpβ(1o
mPoly π
)))) |
56 | | ply1coe.m |
. . . . . . . . . . . . . 14
β’ π = (mulGrpβπ) |
57 | 56, 9 | mgpbas 19907 |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
58 | 57 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΎ β π΅) β π΅ = (Baseβπ)) |
59 | | ssv 3969 |
. . . . . . . . . . . . 13
β’ π΅ β V |
60 | 59 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ πΎ β π΅) β π΅ β V) |
61 | | ovexd 7393 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ πΎ β π΅) β§ (π β V β§ π β V)) β (π(+gβ(mulGrpβ(1o
mPoly π
)))π) β V) |
62 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ) = (.rβπ) |
63 | 7, 1, 62 | ply1mulr 21614 |
. . . . . . . . . . . . . . . 16
β’
(.rβπ) = (.rβ(1o
mPoly π
)) |
64 | 20, 63 | mgpplusg 19905 |
. . . . . . . . . . . . . . 15
β’
(.rβπ) =
(+gβ(mulGrpβ(1o mPoly π
))) |
65 | 56, 62 | mgpplusg 19905 |
. . . . . . . . . . . . . . 15
β’
(.rβπ) = (+gβπ) |
66 | 64, 65 | eqtr3i 2763 |
. . . . . . . . . . . . . 14
β’
(+gβ(mulGrpβ(1o mPoly π
))) = (+gβπ) |
67 | 66 | oveqi 7371 |
. . . . . . . . . . . . 13
β’ (π(+gβ(mulGrpβ(1o
mPoly π
)))π) = (π(+gβπ)π) |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ πΎ β π΅) β§ (π β V β§ π β V)) β (π(+gβ(mulGrpβ(1o
mPoly π
)))π) = (π(+gβπ)π)) |
69 | 21, 53, 55, 58, 60, 61, 68 | mulgpropd 18923 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ πΎ β π΅) β
(.gβ(mulGrpβ(1o mPoly π
))) = β ) |
70 | 69 | oveqd 7375 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΎ β π΅) β ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π) = ((πββ
) β π)) |
71 | 70 | adantr 482 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π) = ((πββ
) β π)) |
72 | 7 | ply1ring 21635 |
. . . . . . . . . . . 12
β’ (π
β Ring β π β Ring) |
73 | 56 | ringmgp 19975 |
. . . . . . . . . . . 12
β’ (π β Ring β π β Mnd) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . 11
β’ (π
β Ring β π β Mnd) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β π β Mnd) |
76 | | elmapi 8790 |
. . . . . . . . . . . 12
β’ (π β (β0
βm 1o) β π:1oβΆβ0) |
77 | | 0lt1o 8451 |
. . . . . . . . . . . 12
β’ β
β 1o |
78 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
β’ ((π:1oβΆβ0
β§ β
β 1o) β (πββ
) β
β0) |
79 | 76, 77, 78 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (β0
βm 1o) β (πββ
) β
β0) |
80 | 79 | adantl 483 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (πββ
) β
β0) |
81 | | ply1coe.x |
. . . . . . . . . . . 12
β’ π = (var1βπ
) |
82 | 81, 7, 9 | vr1cl 21604 |
. . . . . . . . . . 11
β’ (π
β Ring β π β π΅) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β π β π΅) |
84 | 57, 53, 75, 80, 83 | mulgnn0cld 18902 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((πββ
) β π) β π΅) |
85 | 71, 84 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π) β π΅) |
86 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = β
β (πβπ) = (πββ
)) |
87 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = β
β
((1o mVar π
)βπ) = ((1o mVar π
)ββ
)) |
88 | 81 | vr1val 21579 |
. . . . . . . . . . 11
β’ π = ((1o mVar π
)ββ
) |
89 | 87, 88 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = β
β
((1o mVar π
)βπ) = π) |
90 | 86, 89 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = β
β ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)) = ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π)) |
91 | 54, 90 | gsumsn 19736 |
. . . . . . . 8
β’
(((mulGrpβ(1o mPoly π
)) β Mnd β§ β
β V β§
((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π) β π΅)
β ((mulGrpβ(1o mPoly π
))
Ξ£g (π β {β
}
β¦ ((πβπ)(.gβ(mulGrpβ(1o mPoly π
)))((1o mVar π
)βπ)))) = ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π)) |
92 | 51, 52, 85, 91 | syl3anc 1372 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((mulGrpβ(1o mPoly
π
))
Ξ£g (π β {β
} β¦ ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)))) = ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π)) |
93 | 46, 92 | eqtrid 2785 |
. . . . . 6
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((mulGrpβ(1o mPoly
π
))
Ξ£g (π β 1o β¦ ((πβπ)(.gβ(mulGrpβ(1o
mPoly π
)))((1o mVar
π
)βπ)))) = ((πββ
)(.gβ(mulGrpβ(1o
mPoly π
)))π)) |
94 | 44, 93, 71 | 3eqtrd 2777 |
. . . . 5
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
))) = ((πββ
) β π)) |
95 | 18, 94 | oveq12d 7376 |
. . . 4
β’ (((π
β Ring β§ πΎ β π΅) β§ π β (β0
βm 1o)) β ((πΎβπ) Β· (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
)))) = ((π΄β(πββ
)) Β· ((πββ
) β π))) |
96 | 95 | mpteq2dva 5206 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β (π β (β0
βm 1o) β¦ ((πΎβπ) Β· (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
))))) = (π β (β0
βm 1o) β¦ ((π΄β(πββ
)) Β· ((πββ
) β π)))) |
97 | 96 | oveq2d 7374 |
. 2
β’ ((π
β Ring β§ πΎ β π΅) β ((1o mPoly π
) Ξ£g
(π β
(β0 βm 1o) β¦ ((πΎβπ) Β· (π β (β0
βm 1o) β¦ if(π = π, (1rβπ
), (0gβπ
)))))) = ((1o mPoly π
) Ξ£g
(π β
(β0 βm 1o) β¦ ((π΄β(πββ
)) Β· ((πββ
) β π))))) |
98 | | nn0ex 12424 |
. . . . . 6
β’
β0 β V |
99 | 98 | mptex 7174 |
. . . . 5
β’ (π β β0
β¦ ((π΄βπ) Β· (π β π))) β V |
100 | 99 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (π β β0 β¦ ((π΄βπ) Β· (π β π))) β V) |
101 | 7 | fvexi 6857 |
. . . . 5
β’ π β V |
102 | 101 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β π β V) |
103 | | ovexd 7393 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (1o mPoly π
) β V) |
104 | 9, 10 | eqtr3i 2763 |
. . . . 5
β’
(Baseβπ) =
(Baseβ(1o mPoly π
)) |
105 | 104 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (Baseβπ) = (Baseβ(1o mPoly π
))) |
106 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
107 | 7, 1, 106 | ply1plusg 21612 |
. . . . 5
β’
(+gβπ) = (+gβ(1o
mPoly π
)) |
108 | 107 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (+gβπ) =
(+gβ(1o mPoly π
))) |
109 | 100, 102,
103, 105, 108 | gsumpropd 18538 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π)))) = ((1o mPoly π
) Ξ£g
(π β
β0 β¦ ((π΄βπ) Β· (π β π))))) |
110 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
111 | 1, 7, 110 | ply1mpl0 21642 |
. . . 4
β’
(0gβπ) = (0gβ(1o
mPoly π
)) |
112 | 1 | mpllmod 21439 |
. . . . . 6
β’
((1o β Ο β§ π
β Ring) β (1o mPoly
π
) β
LMod) |
113 | 5, 13, 112 | sylancr 588 |
. . . . 5
β’ ((π
β Ring β§ πΎ β π΅) β (1o mPoly π
) β LMod) |
114 | | lmodcmn 20385 |
. . . . 5
β’
((1o mPoly π
) β LMod β (1o mPoly
π
) β
CMnd) |
115 | 113, 114 | syl 17 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (1o mPoly π
) β CMnd) |
116 | 98 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β β0 β
V) |
117 | 7 | ply1lmod 21639 |
. . . . . . 7
β’ (π
β Ring β π β LMod) |
118 | 117 | ad2antrr 725 |
. . . . . 6
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β π β LMod) |
119 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
120 | 16, 9, 7, 119 | coe1f 21598 |
. . . . . . . . 9
β’ (πΎ β π΅ β π΄:β0βΆ(Baseβπ
)) |
121 | 120 | adantl 483 |
. . . . . . . 8
β’ ((π
β Ring β§ πΎ β π΅) β π΄:β0βΆ(Baseβπ
)) |
122 | 121 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β (π΄βπ) β (Baseβπ
)) |
123 | 7 | ply1sca 21640 |
. . . . . . . . . 10
β’ (π
β Ring β π
= (Scalarβπ)) |
124 | 123 | eqcomd 2739 |
. . . . . . . . 9
β’ (π
β Ring β
(Scalarβπ) = π
) |
125 | 124 | ad2antrr 725 |
. . . . . . . 8
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β
(Scalarβπ) = π
) |
126 | 125 | fveq2d 6847 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β
(Baseβ(Scalarβπ)) = (Baseβπ
)) |
127 | 122, 126 | eleqtrrd 2837 |
. . . . . 6
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β (π΄βπ) β (Baseβ(Scalarβπ))) |
128 | 74 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β π β Mnd) |
129 | | simpr 486 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β π β
β0) |
130 | 82 | ad2antrr 725 |
. . . . . . 7
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β π β π΅) |
131 | 57, 53, 128, 129, 130 | mulgnn0cld 18902 |
. . . . . 6
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β (π β π) β π΅) |
132 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
133 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
134 | 9, 132, 11, 133 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ (π΄βπ) β (Baseβ(Scalarβπ)) β§ (π β π) β π΅) β ((π΄βπ) Β· (π β π)) β π΅) |
135 | 118, 127,
131, 134 | syl3anc 1372 |
. . . . 5
β’ (((π
β Ring β§ πΎ β π΅) β§ π β β0) β ((π΄βπ) Β· (π β π)) β π΅) |
136 | 135 | fmpttd 7064 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (π β β0 β¦ ((π΄βπ) Β· (π β π))):β0βΆπ΅) |
137 | 7, 81, 9, 11, 56, 53, 16 | ply1coefsupp 21682 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (π β β0 β¦ ((π΄βπ) Β· (π β π))) finSupp (0gβπ)) |
138 | | eqid 2733 |
. . . . . 6
β’ (π β (β0
βm 1o) β¦ (πββ
)) = (π β (β0
βm 1o) β¦ (πββ
)) |
139 | 40, 98, 26, 138 | mapsnf1o2 8835 |
. . . . 5
β’ (π β (β0
βm 1o) β¦ (πββ
)):(β0
βm 1o)β1-1-ontoββ0 |
140 | 139 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β (π β (β0
βm 1o) β¦ (πββ
)):(β0
βm 1o)β1-1-ontoββ0) |
141 | 10, 111, 115, 116, 136, 137, 140 | gsumf1o 19698 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β ((1o mPoly π
) Ξ£g
(π β
β0 β¦ ((π΄βπ) Β· (π β π)))) = ((1o mPoly π
) Ξ£g
((π β
β0 β¦ ((π΄βπ) Β· (π β π))) β (π β (β0
βm 1o) β¦ (πββ
))))) |
142 | | eqidd 2734 |
. . . . 5
β’ ((π
β Ring β§ πΎ β π΅) β (π β (β0
βm 1o) β¦ (πββ
)) = (π β (β0
βm 1o) β¦ (πββ
))) |
143 | | eqidd 2734 |
. . . . 5
β’ ((π
β Ring β§ πΎ β π΅) β (π β β0 β¦ ((π΄βπ) Β· (π β π))) = (π β β0 β¦ ((π΄βπ) Β· (π β π)))) |
144 | | fveq2 6843 |
. . . . . 6
β’ (π = (πββ
) β (π΄βπ) = (π΄β(πββ
))) |
145 | | oveq1 7365 |
. . . . . 6
β’ (π = (πββ
) β (π β π) = ((πββ
) β π)) |
146 | 144, 145 | oveq12d 7376 |
. . . . 5
β’ (π = (πββ
) β ((π΄βπ) Β· (π β π)) = ((π΄β(πββ
)) Β· ((πββ
) β π))) |
147 | 80, 142, 143, 146 | fmptco 7076 |
. . . 4
β’ ((π
β Ring β§ πΎ β π΅) β ((π β β0 β¦ ((π΄βπ) Β· (π β π))) β (π β (β0
βm 1o) β¦ (πββ
))) = (π β (β0
βm 1o) β¦ ((π΄β(πββ
)) Β· ((πββ
) β π)))) |
148 | 147 | oveq2d 7374 |
. . 3
β’ ((π
β Ring β§ πΎ β π΅) β ((1o mPoly π
) Ξ£g
((π β
β0 β¦ ((π΄βπ) Β· (π β π))) β (π β (β0
βm 1o) β¦ (πββ
)))) = ((1o mPoly
π
)
Ξ£g (π β (β0
βm 1o) β¦ ((π΄β(πββ
)) Β· ((πββ
) β π))))) |
149 | 109, 141,
148 | 3eqtrrd 2778 |
. 2
β’ ((π
β Ring β§ πΎ β π΅) β ((1o mPoly π
) Ξ£g
(π β
(β0 βm 1o) β¦ ((π΄β(πββ
)) Β· ((πββ
) β π)))) = (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π))))) |
150 | 15, 97, 149 | 3eqtrd 2777 |
1
β’ ((π
β Ring β§ πΎ β π΅) β πΎ = (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π))))) |