Step | Hyp | Ref
| Expression |
1 | | evls1fpws.r |
. . . . 5
β’ (π β π
β (SubRingβπ)) |
2 | | ressply1evl.u |
. . . . . 6
β’ π = (π βΎs π
) |
3 | 2 | subrgring 20267 |
. . . . 5
β’ (π
β (SubRingβπ) β π β Ring) |
4 | 1, 3 | syl 17 |
. . . 4
β’ (π β π β Ring) |
5 | | evls1fpws.y |
. . . 4
β’ (π β π β π΅) |
6 | | ressply1evl.w |
. . . . 5
β’ π = (Poly1βπ) |
7 | | eqid 2733 |
. . . . 5
β’
(var1βπ) = (var1βπ) |
8 | | ressply1evl.b |
. . . . 5
β’ π΅ = (Baseβπ) |
9 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
10 | | eqid 2733 |
. . . . 5
β’
(mulGrpβπ) =
(mulGrpβπ) |
11 | | eqid 2733 |
. . . . 5
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
12 | | evls1fpws.a |
. . . . 5
β’ π΄ = (coe1βπ) |
13 | 6, 7, 8, 9, 10, 11, 12 | ply1coe 21690 |
. . . 4
β’ ((π β Ring β§ π β π΅) β π = (π Ξ£g (π β β0
β¦ ((π΄βπ)(
Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ)))))) |
14 | 4, 5, 13 | syl2anc 585 |
. . 3
β’ (π β π = (π Ξ£g (π β β0
β¦ ((π΄βπ)(
Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ)))))) |
15 | 14 | fveq2d 6850 |
. 2
β’ (π β (πβπ) = (πβ(π Ξ£g (π β β0
β¦ ((π΄βπ)(
Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ))))))) |
16 | | ressply1evl.q |
. . . 4
β’ π = (π evalSub1 π
) |
17 | | ressply1evl.k |
. . . 4
β’ πΎ = (Baseβπ) |
18 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
19 | | eqid 2733 |
. . . 4
β’ (π βs πΎ) = (π βs πΎ) |
20 | | evls1fpws.s |
. . . 4
β’ (π β π β CRing) |
21 | 6 | ply1lmod 21646 |
. . . . . . 7
β’ (π β Ring β π β LMod) |
22 | 4, 21 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
23 | 22 | adantr 482 |
. . . . 5
β’ ((π β§ π β β0) β π β LMod) |
24 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
25 | 12, 8, 6, 24 | coe1fvalcl 21606 |
. . . . . . 7
β’ ((π β π΅ β§ π β β0) β (π΄βπ) β (Baseβπ)) |
26 | 5, 25 | sylan 581 |
. . . . . 6
β’ ((π β§ π β β0) β (π΄βπ) β (Baseβπ)) |
27 | 6 | ply1sca 21647 |
. . . . . . . . 9
β’ (π β Ring β π = (Scalarβπ)) |
28 | 4, 27 | syl 17 |
. . . . . . . 8
β’ (π β π = (Scalarβπ)) |
29 | 28 | fveq2d 6850 |
. . . . . . 7
β’ (π β (Baseβπ) =
(Baseβ(Scalarβπ))) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β0) β
(Baseβπ) =
(Baseβ(Scalarβπ))) |
31 | 26, 30 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π β β0) β (π΄βπ) β (Baseβ(Scalarβπ))) |
32 | 10, 8 | mgpbas 19910 |
. . . . . 6
β’ π΅ =
(Baseβ(mulGrpβπ)) |
33 | 6 | ply1ring 21642 |
. . . . . . . . 9
β’ (π β Ring β π β Ring) |
34 | 4, 33 | syl 17 |
. . . . . . . 8
β’ (π β π β Ring) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β0) β π β Ring) |
36 | 10 | ringmgp 19978 |
. . . . . . 7
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
37 | 35, 36 | syl 17 |
. . . . . 6
β’ ((π β§ π β β0) β
(mulGrpβπ) β
Mnd) |
38 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β0) |
39 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β0) β π β Ring) |
40 | 7, 6, 8 | vr1cl 21611 |
. . . . . . 7
β’ (π β Ring β
(var1βπ)
β π΅) |
41 | 39, 40 | syl 17 |
. . . . . 6
β’ ((π β§ π β β0) β
(var1βπ)
β π΅) |
42 | 32, 11, 37, 38, 41 | mulgnn0cld 18905 |
. . . . 5
β’ ((π β§ π β β0) β (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) |
43 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
44 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
45 | 8, 43, 9, 44 | lmodvscl 20383 |
. . . . 5
β’ ((π β LMod β§ (π΄βπ) β (Baseβ(Scalarβπ)) β§ (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) β π΅) |
46 | 23, 31, 42, 45 | syl3anc 1372 |
. . . 4
β’ ((π β§ π β β0) β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) β π΅) |
47 | | ssidd 3971 |
. . . 4
β’ (π β β0
β β0) |
48 | | fvexd 6861 |
. . . . 5
β’ (π β (0gβπ) β V) |
49 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
50 | | oveq1 7368 |
. . . . . 6
β’ (π = π β (π(.gβ(mulGrpβπ))(var1βπ)) = (π(.gβ(mulGrpβπ))(var1βπ))) |
51 | 49, 50 | oveq12d 7379 |
. . . . 5
β’ (π = π β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) |
52 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
53 | 12, 8, 6, 52 | coe1ae0 21610 |
. . . . . . 7
β’ (π β π΅ β βπ β β0 βπ β β0
(π < π β (π΄βπ) = (0gβπ))) |
54 | 5, 53 | syl 17 |
. . . . . 6
β’ (π β βπ β β0 βπ β β0
(π < π β (π΄βπ) = (0gβπ))) |
55 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β (π΄βπ) = (0gβπ)) |
56 | 28 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β π = (Scalarβπ)) |
57 | 56 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β
(0gβπ) =
(0gβ(Scalarβπ))) |
58 | 55, 57 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β (π΄βπ) = (0gβ(Scalarβπ))) |
59 | 58 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) =
((0gβ(Scalarβπ))( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) |
60 | 22 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β π β LMod) |
61 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (mulGrpβπ) β Mnd) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
(mulGrpβπ) β
Mnd) |
63 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β π β
β0) |
64 | 4, 40 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β
(var1βπ)
β π΅) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β
(var1βπ)
β π΅) |
66 | 32, 11, 62, 63, 65 | mulgnn0cld 18905 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) |
67 | 66 | ad4ant13 750 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) |
68 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
69 | 8, 43, 9, 68, 18 | lmod0vs 20399 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) β
((0gβ(Scalarβπ))( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)) |
70 | 60, 67, 69 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β
((0gβ(Scalarβπ))( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)) |
71 | 59, 70 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β§ π β β0) β§ π β β0)
β§ (π΄βπ) = (0gβπ)) β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)) |
72 | 71 | ex 414 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β β0)
β ((π΄βπ) = (0gβπ) β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ))) |
73 | 72 | imim2d 57 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β β0)
β ((π < π β (π΄βπ) = (0gβπ)) β (π < π β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)))) |
74 | 73 | ralimdva 3161 |
. . . . . . 7
β’ ((π β§ π β β0) β
(βπ β
β0 (π <
π β (π΄βπ) = (0gβπ)) β βπ β β0 (π < π β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)))) |
75 | 74 | reximdva 3162 |
. . . . . 6
β’ (π β (βπ β β0 βπ β β0
(π < π β (π΄βπ) = (0gβπ)) β βπ β β0 βπ β β0
(π < π β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ)))) |
76 | 54, 75 | mpd 15 |
. . . . 5
β’ (π β βπ β β0 βπ β β0
(π < π β ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))) = (0gβπ))) |
77 | 48, 46, 51, 76 | mptnn0fsuppd 13912 |
. . . 4
β’ (π β (π β β0 β¦ ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) finSupp
(0gβπ)) |
78 | 16, 17, 6, 18, 2, 19, 8, 20, 1, 46, 47, 77 | evls1gsumadd 21713 |
. . 3
β’ (π β (πβ(π Ξ£g (π β β0
β¦ ((π΄βπ)(
Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ)))))) = ((π βs πΎ) Ξ£g (π β β0
β¦ (πβ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))))))) |
79 | 16, 17, 19, 2, 6 | evls1rhm 21711 |
. . . . . . . . 9
β’ ((π β CRing β§ π
β (SubRingβπ)) β π β (π RingHom (π βs πΎ))) |
80 | 20, 1, 79 | syl2anc 585 |
. . . . . . . 8
β’ (π β π β (π RingHom (π βs πΎ))) |
81 | 80 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β0) β π β (π RingHom (π βs πΎ))) |
82 | | eqid 2733 |
. . . . . . . . . 10
β’
(algScβπ) =
(algScβπ) |
83 | 82, 43, 34, 22, 44, 8 | asclf 21308 |
. . . . . . . . 9
β’ (π β (algScβπ):(Baseβ(Scalarβπ))βΆπ΅) |
84 | 83 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(algScβπ):(Baseβ(Scalarβπ))βΆπ΅) |
85 | 84, 31 | ffvelcdmd 7040 |
. . . . . . 7
β’ ((π β§ π β β0) β
((algScβπ)β(π΄βπ)) β π΅) |
86 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ) = (.rβπ) |
87 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(π βs πΎ)) = (.rβ(π βs πΎ)) |
88 | 8, 86, 87 | rhmmul 20169 |
. . . . . . 7
β’ ((π β (π RingHom (π βs πΎ)) β§ ((algScβπ)β(π΄βπ)) β π΅ β§ (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) β (πβ(((algScβπ)β(π΄βπ))(.rβπ)(π(.gβ(mulGrpβπ))(var1βπ)))) = ((πβ((algScβπ)β(π΄βπ)))(.rβ(π βs πΎ))(πβ(π(.gβ(mulGrpβπ))(var1βπ))))) |
89 | 81, 85, 42, 88 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π β β0) β (πβ(((algScβπ)β(π΄βπ))(.rβπ)(π(.gβ(mulGrpβπ))(var1βπ)))) = ((πβ((algScβπ)β(π΄βπ)))(.rβ(π βs πΎ))(πβ(π(.gβ(mulGrpβπ))(var1βπ))))) |
90 | 2 | subrgcrng 20268 |
. . . . . . . . . . 11
β’ ((π β CRing β§ π
β (SubRingβπ)) β π β CRing) |
91 | 20, 1, 90 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π β CRing) |
92 | 6 | ply1assa 21593 |
. . . . . . . . . 10
β’ (π β CRing β π β AssAlg) |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
β’ (π β π β AssAlg) |
94 | 93 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β AssAlg) |
95 | 82, 43, 44, 8, 86, 9 | asclmul1 21312 |
. . . . . . . 8
β’ ((π β AssAlg β§ (π΄βπ) β (Baseβ(Scalarβπ)) β§ (π(.gβ(mulGrpβπ))(var1βπ)) β π΅) β (((algScβπ)β(π΄βπ))(.rβπ)(π(.gβ(mulGrpβπ))(var1βπ))) = ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) |
96 | 94, 31, 42, 95 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β β0) β
(((algScβπ)β(π΄βπ))(.rβπ)(π(.gβ(mulGrpβπ))(var1βπ))) = ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) |
97 | 96 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ π β β0) β (πβ(((algScβπ)β(π΄βπ))(.rβπ)(π(.gβ(mulGrpβπ))(var1βπ)))) = (πβ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))))) |
98 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(π
βs πΎ)) = (Baseβ(π βs πΎ)) |
99 | 20 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β CRing) |
100 | 17 | fvexi 6860 |
. . . . . . . . 9
β’ πΎ β V |
101 | 100 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β β0) β πΎ β V) |
102 | 8, 98 | rhmf 20168 |
. . . . . . . . . 10
β’ (π β (π RingHom (π βs πΎ)) β π:π΅βΆ(Baseβ(π βs πΎ))) |
103 | 81, 102 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π:π΅βΆ(Baseβ(π βs πΎ))) |
104 | 103, 85 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πβ((algScβπ)β(π΄βπ))) β (Baseβ(π βs πΎ))) |
105 | 103, 42 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πβ(π(.gβ(mulGrpβπ))(var1βπ))) β (Baseβ(π βs πΎ))) |
106 | | evls1fpws.1 |
. . . . . . . 8
β’ Β· =
(.rβπ) |
107 | 19, 98, 99, 101, 104, 105, 106, 87 | pwsmulrval 17381 |
. . . . . . 7
β’ ((π β§ π β β0) β ((πβ((algScβπ)β(π΄βπ)))(.rβ(π βs πΎ))(πβ(π(.gβ(mulGrpβπ))(var1βπ)))) = ((πβ((algScβπ)β(π΄βπ))) βf Β· (πβ(π(.gβ(mulGrpβπ))(var1βπ))))) |
108 | 19, 17, 98, 99, 101, 104 | pwselbas 17379 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (πβ((algScβπ)β(π΄βπ))):πΎβΆπΎ) |
109 | 108 | ffnd 6673 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πβ((algScβπ)β(π΄βπ))) Fn πΎ) |
110 | 19, 17, 98, 99, 101, 105 | pwselbas 17379 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (πβ(π(.gβ(mulGrpβπ))(var1βπ))):πΎβΆπΎ) |
111 | 110 | ffnd 6673 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πβ(π(.gβ(mulGrpβπ))(var1βπ))) Fn πΎ) |
112 | | inidm 4182 |
. . . . . . . 8
β’ (πΎ β© πΎ) = πΎ |
113 | 20 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β π β CRing) |
114 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β π
β (SubRingβπ)) |
115 | 17 | subrgss 20265 |
. . . . . . . . . . . . . 14
β’ (π
β (SubRingβπ) β π
β πΎ) |
116 | 1, 115 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π
β πΎ) |
117 | 2, 17 | ressbas2 17128 |
. . . . . . . . . . . . 13
β’ (π
β πΎ β π
= (Baseβπ)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π
= (Baseβπ)) |
119 | 118 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π
= (Baseβπ)) |
120 | 26, 119 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π΄βπ) β π
) |
121 | 120 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β (π΄βπ) β π
) |
122 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β π₯ β πΎ) |
123 | 16, 6, 2, 17, 82, 113, 114, 121, 122 | evls1scafv 32324 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΎ) β ((πβ((algScβπ)β(π΄βπ)))βπ₯) = (π΄βπ)) |
124 | | evls1fpws.2 |
. . . . . . . . 9
β’ β =
(.gβ(mulGrpβπ)) |
125 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β π β β0) |
126 | 16, 2, 6, 7, 17, 11, 124, 113, 114, 125, 122 | evls1varpwval 32326 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΎ) β ((πβ(π(.gβ(mulGrpβπ))(var1βπ)))βπ₯) = (π β π₯)) |
127 | 109, 111,
101, 101, 112, 123, 126 | offval 7630 |
. . . . . . 7
β’ ((π β§ π β β0) β ((πβ((algScβπ)β(π΄βπ))) βf Β· (πβ(π(.gβ(mulGrpβπ))(var1βπ)))) = (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) |
128 | 107, 127 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β β0) β ((πβ((algScβπ)β(π΄βπ)))(.rβ(π βs πΎ))(πβ(π(.gβ(mulGrpβπ))(var1βπ)))) = (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) |
129 | 89, 97, 128 | 3eqtr3d 2781 |
. . . . 5
β’ ((π β§ π β β0) β (πβ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))) = (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) |
130 | 129 | mpteq2dva 5209 |
. . . 4
β’ (π β (π β β0 β¦ (πβ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ))))) = (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))))) |
131 | 130 | oveq2d 7377 |
. . 3
β’ (π β ((π βs πΎ) Ξ£g (π β β0
β¦ (πβ((π΄βπ)( Β·π
βπ)(π(.gβ(mulGrpβπ))(var1βπ)))))) = ((π βs πΎ) Ξ£g (π β β0
β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))))) |
132 | | eqid 2733 |
. . . 4
β’
(0gβ(π βs πΎ)) = (0gβ(π βs πΎ)) |
133 | 100 | a1i 11 |
. . . 4
β’ (π β πΎ β V) |
134 | | nn0ex 12427 |
. . . . 5
β’
β0 β V |
135 | 134 | a1i 11 |
. . . 4
β’ (π β β0 β
V) |
136 | 20 | crngringd 19985 |
. . . . 5
β’ (π β π β Ring) |
137 | 136 | ringcmnd 20013 |
. . . 4
β’ (π β π β CMnd) |
138 | 136 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΎ) β π β Ring) |
139 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π
β (SubRingβπ)) |
140 | 139, 115 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π
β πΎ) |
141 | 140, 120 | sseldd 3949 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π΄βπ) β πΎ) |
142 | 141 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΎ) β (π΄βπ) β πΎ) |
143 | | eqid 2733 |
. . . . . . . . . 10
β’
(mulGrpβπ) =
(mulGrpβπ) |
144 | 143, 17 | mgpbas 19910 |
. . . . . . . . 9
β’ πΎ =
(Baseβ(mulGrpβπ)) |
145 | 143 | ringmgp 19978 |
. . . . . . . . . . 11
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
146 | 136, 145 | syl 17 |
. . . . . . . . . 10
β’ (π β (mulGrpβπ) β Mnd) |
147 | 146 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΎ) β (mulGrpβπ) β Mnd) |
148 | 144, 124,
147, 125, 122 | mulgnn0cld 18905 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΎ) β (π β π₯) β πΎ) |
149 | 17, 106, 138, 142, 148 | ringcld 19994 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π₯ β πΎ) β ((π΄βπ) Β· (π β π₯)) β πΎ) |
150 | 149 | 3impa 1111 |
. . . . . 6
β’ ((π β§ π β β0 β§ π₯ β πΎ) β ((π΄βπ) Β· (π β π₯)) β πΎ) |
151 | 150 | 3com23 1127 |
. . . . 5
β’ ((π β§ π₯ β πΎ β§ π β β0) β ((π΄βπ) Β· (π β π₯)) β πΎ) |
152 | 151 | 3expb 1121 |
. . . 4
β’ ((π β§ (π₯ β πΎ β§ π β β0)) β ((π΄βπ) Β· (π β π₯)) β πΎ) |
153 | 135 | mptexd 7178 |
. . . . 5
β’ (π β (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) β V) |
154 | | funmpt 6543 |
. . . . . 6
β’ Fun
(π β
β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) |
155 | 154 | a1i 11 |
. . . . 5
β’ (π β Fun (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))))) |
156 | | fvexd 6861 |
. . . . 5
β’ (π β
(0gβ(π
βs πΎ)) β V) |
157 | 12, 8, 6, 52 | coe1sfi 21607 |
. . . . . . 7
β’ (π β π΅ β π΄ finSupp (0gβπ)) |
158 | 5, 157 | syl 17 |
. . . . . 6
β’ (π β π΄ finSupp (0gβπ)) |
159 | 158 | fsuppimpd 9319 |
. . . . 5
β’ (π β (π΄ supp (0gβπ)) β Fin) |
160 | 12, 8, 6, 24 | coe1f 21605 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΅ β π΄:β0βΆ(Baseβπ)) |
161 | 5, 160 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄:β0βΆ(Baseβπ)) |
162 | 161 | ffnd 6673 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ Fn β0) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β π΄ Fn β0) |
164 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β β0
β V) |
165 | | fvexd 6861 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β
(0gβπ)
β V) |
166 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β π β (β0 β (π΄ supp (0gβπ)))) |
167 | 163, 164,
165, 166 | fvdifsupp 31652 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (π΄βπ) = (0gβπ)) |
168 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ) = (0gβπ) |
169 | 2, 168 | subrg0 20271 |
. . . . . . . . . . . . . . 15
β’ (π
β (SubRingβπ) β
(0gβπ) =
(0gβπ)) |
170 | 1, 169 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (0gβπ) = (0gβπ)) |
171 | 170 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β
(0gβπ) =
(0gβπ)) |
172 | 167, 171 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (π΄βπ) = (0gβπ)) |
173 | 172 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β (π΄βπ) = (0gβπ)) |
174 | 173 | oveq1d 7376 |
. . . . . . . . . 10
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β ((π΄βπ) Β· (π β π₯)) = ((0gβπ) Β· (π β π₯))) |
175 | 136 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β π β Ring) |
176 | 175, 145 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β (mulGrpβπ) β Mnd) |
177 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β π β (β0 β (π΄ supp (0gβπ)))) |
178 | 177 | eldifad 3926 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β π β β0) |
179 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β π₯ β πΎ) |
180 | 144, 124,
176, 178, 179 | mulgnn0cld 18905 |
. . . . . . . . . . 11
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β (π β π₯) β πΎ) |
181 | 17, 106, 168 | ringlz 20019 |
. . . . . . . . . . 11
β’ ((π β Ring β§ (π β π₯) β πΎ) β ((0gβπ) Β· (π β π₯)) = (0gβπ)) |
182 | 175, 180,
181 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β ((0gβπ) Β· (π β π₯)) = (0gβπ)) |
183 | 174, 182 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ π β (β0 β (π΄ supp (0gβπ)))) β§ π₯ β πΎ) β ((π΄βπ) Β· (π β π₯)) = (0gβπ)) |
184 | 183 | mpteq2dva 5209 |
. . . . . . . 8
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))) = (π₯ β πΎ β¦ (0gβπ))) |
185 | | fconstmpt 5698 |
. . . . . . . 8
β’ (πΎ Γ
{(0gβπ)})
= (π₯ β πΎ β¦
(0gβπ)) |
186 | 184, 185 | eqtr4di 2791 |
. . . . . . 7
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))) = (πΎ Γ {(0gβπ)})) |
187 | 137 | cmnmndd 19594 |
. . . . . . . . 9
β’ (π β π β Mnd) |
188 | 19, 168 | pws0g 18600 |
. . . . . . . . 9
β’ ((π β Mnd β§ πΎ β V) β (πΎ Γ
{(0gβπ)})
= (0gβ(π
βs πΎ))) |
189 | 187, 133,
188 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΎ Γ {(0gβπ)}) =
(0gβ(π
βs πΎ))) |
190 | 189 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (πΎ Γ {(0gβπ)}) =
(0gβ(π
βs πΎ))) |
191 | 186, 190 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β (β0 β (π΄ supp (0gβπ)))) β (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))) = (0gβ(π βs πΎ))) |
192 | 191, 135 | suppss2 8135 |
. . . . 5
β’ (π β ((π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) supp (0gβ(π βs πΎ))) β (π΄ supp (0gβπ))) |
193 | | suppssfifsupp 9328 |
. . . . 5
β’ ((((π β β0
β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) β V β§ Fun (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) β§ (0gβ(π βs πΎ)) β V) β§ ((π΄ supp (0gβπ)) β Fin β§ ((π β β0
β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) supp (0gβ(π βs πΎ))) β (π΄ supp (0gβπ)))) β (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) finSupp (0gβ(π βs πΎ))) |
194 | 153, 155,
156, 159, 192, 193 | syl32anc 1379 |
. . . 4
β’ (π β (π β β0 β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯)))) finSupp (0gβ(π βs πΎ))) |
195 | 19, 17, 132, 133, 135, 137, 152, 194 | pwsgsum 19767 |
. . 3
β’ (π β ((π βs πΎ) Ξ£g (π β β0
β¦ (π₯ β πΎ β¦ ((π΄βπ) Β· (π β π₯))))) = (π₯ β πΎ β¦ (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π₯)))))) |
196 | 78, 131, 195 | 3eqtrd 2777 |
. 2
β’ (π β (πβ(π Ξ£g (π β β0
β¦ ((π΄βπ)(
Β·π βπ)(π(.gβ(mulGrpβπ))(var1βπ)))))) = (π₯ β πΎ β¦ (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π₯)))))) |
197 | 15, 196 | eqtrd 2773 |
1
β’ (π β (πβπ) = (π₯ β πΎ β¦ (π Ξ£g (π β β0
β¦ ((π΄βπ) Β· (π β π₯)))))) |