Step | Hyp | Ref
| Expression |
1 | | evlslem1.b |
. . 3
β’ π΅ = (Baseβπ) |
2 | | eqid 2732 |
. . 3
β’
(1rβπ) = (1rβπ) |
3 | | eqid 2732 |
. . 3
β’
(1rβπ) = (1rβπ) |
4 | | eqid 2732 |
. . 3
β’
(.rβπ) = (.rβπ) |
5 | | evlslem1.m |
. . 3
β’ Β· =
(.rβπ) |
6 | | evlslem1.i |
. . . 4
β’ (π β πΌ β π) |
7 | | evlslem1.r |
. . . . 5
β’ (π β π
β CRing) |
8 | 7 | crngringd 20062 |
. . . 4
β’ (π β π
β Ring) |
9 | | evlslem1.p |
. . . . 5
β’ π = (πΌ mPoly π
) |
10 | 9 | mplring 21569 |
. . . 4
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
11 | 6, 8, 10 | syl2anc 584 |
. . 3
β’ (π β π β Ring) |
12 | | evlslem1.s |
. . . 4
β’ (π β π β CRing) |
13 | 12 | crngringd 20062 |
. . 3
β’ (π β π β Ring) |
14 | | 2fveq3 6893 |
. . . . . 6
β’ (π₯ = (1rβπ
) β (πΈβ(π΄βπ₯)) = (πΈβ(π΄β(1rβπ
)))) |
15 | | fveq2 6888 |
. . . . . 6
β’ (π₯ = (1rβπ
) β (πΉβπ₯) = (πΉβ(1rβπ
))) |
16 | 14, 15 | eqeq12d 2748 |
. . . . 5
β’ (π₯ = (1rβπ
) β ((πΈβ(π΄βπ₯)) = (πΉβπ₯) β (πΈβ(π΄β(1rβπ
))) = (πΉβ(1rβπ
)))) |
17 | | evlslem1.d |
. . . . . . . . 9
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
18 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
19 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
20 | | evlslem1.a |
. . . . . . . . 9
β’ π΄ = (algScβπ) |
21 | 6 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
)) β πΌ β π) |
22 | 8 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
)) β π
β Ring) |
23 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
)) β π₯ β (Baseβπ
)) |
24 | 9, 17, 18, 19, 20, 21, 22, 23 | mplascl 21616 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β (π΄βπ₯) = (π¦ β π· β¦ if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
)))) |
25 | 24 | fveq2d 6892 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (πΈβ(π΄βπ₯)) = (πΈβ(π¦ β π· β¦ if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
))))) |
26 | | evlslem1.c |
. . . . . . . 8
β’ πΆ = (Baseβπ) |
27 | | evlslem1.t |
. . . . . . . 8
β’ π = (mulGrpβπ) |
28 | | evlslem1.x |
. . . . . . . 8
β’ β =
(.gβπ) |
29 | | evlslem1.v |
. . . . . . . 8
β’ π = (πΌ mVar π
) |
30 | | evlslem1.e |
. . . . . . . 8
β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
31 | 7 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β π
β CRing) |
32 | 12 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β π β CRing) |
33 | | evlslem1.f |
. . . . . . . . 9
β’ (π β πΉ β (π
RingHom π)) |
34 | 33 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β πΉ β (π
RingHom π)) |
35 | | evlslem1.g |
. . . . . . . . 9
β’ (π β πΊ:πΌβΆπΆ) |
36 | 35 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β πΊ:πΌβΆπΆ) |
37 | 17 | psrbag0 21614 |
. . . . . . . . . 10
β’ (πΌ β π β (πΌ Γ {0}) β π·) |
38 | 6, 37 | syl 17 |
. . . . . . . . 9
β’ (π β (πΌ Γ {0}) β π·) |
39 | 38 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β (πΌ Γ {0}) β π·) |
40 | 9, 1, 26, 19, 17, 27, 28, 5, 29, 30, 21, 31, 32, 34, 36, 18, 39, 23 | evlslem3 21634 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β (πΈβ(π¦ β π· β¦ if(π¦ = (πΌ Γ {0}), π₯, (0gβπ
)))) = ((πΉβπ₯) Β· (π Ξ£g ((πΌ Γ {0})
βf β πΊ)))) |
41 | | 0zd 12566 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΌ) β 0 β β€) |
42 | | fvexd 6903 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΌ) β (πΊβπ₯) β V) |
43 | | fconstmpt 5736 |
. . . . . . . . . . . . . . 15
β’ (πΌ Γ {0}) = (π₯ β πΌ β¦ 0) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ Γ {0}) = (π₯ β πΌ β¦ 0)) |
45 | 35 | feqmptd 6957 |
. . . . . . . . . . . . . 14
β’ (π β πΊ = (π₯ β πΌ β¦ (πΊβπ₯))) |
46 | 6, 41, 42, 44, 45 | offval2 7686 |
. . . . . . . . . . . . 13
β’ (π β ((πΌ Γ {0}) βf β πΊ) = (π₯ β πΌ β¦ (0 β (πΊβπ₯)))) |
47 | 35 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΌ) β (πΊβπ₯) β πΆ) |
48 | 27, 26 | mgpbas 19987 |
. . . . . . . . . . . . . . . 16
β’ πΆ = (Baseβπ) |
49 | 27, 3 | ringidval 20000 |
. . . . . . . . . . . . . . . 16
β’
(1rβπ) = (0gβπ) |
50 | 48, 49, 28 | mulg0 18951 |
. . . . . . . . . . . . . . 15
β’ ((πΊβπ₯) β πΆ β (0 β (πΊβπ₯)) = (1rβπ)) |
51 | 47, 50 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΌ) β (0 β (πΊβπ₯)) = (1rβπ)) |
52 | 51 | mpteq2dva 5247 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β πΌ β¦ (0 β (πΊβπ₯))) = (π₯ β πΌ β¦ (1rβπ))) |
53 | 46, 52 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (π β ((πΌ Γ {0}) βf β πΊ) = (π₯ β πΌ β¦ (1rβπ))) |
54 | 53 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (π β (π Ξ£g ((πΌ Γ {0})
βf β πΊ)) = (π Ξ£g (π₯ β πΌ β¦ (1rβπ)))) |
55 | 27 | crngmgp 20057 |
. . . . . . . . . . . . . 14
β’ (π β CRing β π β CMnd) |
56 | 12, 55 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β CMnd) |
57 | 56 | cmnmndd 19666 |
. . . . . . . . . . . 12
β’ (π β π β Mnd) |
58 | 49 | gsumz 18713 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ πΌ β π) β (π Ξ£g (π₯ β πΌ β¦ (1rβπ))) = (1rβπ)) |
59 | 57, 6, 58 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (π Ξ£g (π₯ β πΌ β¦ (1rβπ))) = (1rβπ)) |
60 | 54, 59 | eqtrd 2772 |
. . . . . . . . . 10
β’ (π β (π Ξ£g ((πΌ Γ {0})
βf β πΊ)) = (1rβπ)) |
61 | 60 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
)) β (π Ξ£g ((πΌ Γ {0})
βf β πΊ)) = (1rβπ)) |
62 | 61 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΉβπ₯) Β· (π Ξ£g ((πΌ Γ {0})
βf β πΊ))) = ((πΉβπ₯) Β·
(1rβπ))) |
63 | 19, 26 | rhmf 20255 |
. . . . . . . . . . 11
β’ (πΉ β (π
RingHom π) β πΉ:(Baseβπ
)βΆπΆ) |
64 | 33, 63 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:(Baseβπ
)βΆπΆ) |
65 | 64 | ffvelcdmda 7083 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ
)) β (πΉβπ₯) β πΆ) |
66 | 26, 5, 3 | ringridm 20080 |
. . . . . . . . 9
β’ ((π β Ring β§ (πΉβπ₯) β πΆ) β ((πΉβπ₯) Β·
(1rβπ)) =
(πΉβπ₯)) |
67 | 13, 65, 66 | syl2an2r 683 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΉβπ₯) Β·
(1rβπ)) =
(πΉβπ₯)) |
68 | 62, 67 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΉβπ₯) Β· (π Ξ£g ((πΌ Γ {0})
βf β πΊ))) = (πΉβπ₯)) |
69 | 25, 40, 68 | 3eqtrd 2776 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ
)) β (πΈβ(π΄βπ₯)) = (πΉβπ₯)) |
70 | 69 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ₯ β (Baseβπ
)(πΈβ(π΄βπ₯)) = (πΉβπ₯)) |
71 | | eqid 2732 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
72 | 19, 71 | ringidcl 20076 |
. . . . . 6
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
73 | 8, 72 | syl 17 |
. . . . 5
β’ (π β (1rβπ
) β (Baseβπ
)) |
74 | 16, 70, 73 | rspcdva 3613 |
. . . 4
β’ (π β (πΈβ(π΄β(1rβπ
))) = (πΉβ(1rβπ
))) |
75 | 9 | mplassa 21572 |
. . . . . . . . 9
β’ ((πΌ β π β§ π
β CRing) β π β AssAlg) |
76 | 6, 7, 75 | syl2anc 584 |
. . . . . . . 8
β’ (π β π β AssAlg) |
77 | | eqid 2732 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
78 | 20, 77 | asclrhm 21435 |
. . . . . . . 8
β’ (π β AssAlg β π΄ β ((Scalarβπ) RingHom π)) |
79 | 76, 78 | syl 17 |
. . . . . . 7
β’ (π β π΄ β ((Scalarβπ) RingHom π)) |
80 | 9, 6, 7 | mplsca 21563 |
. . . . . . . 8
β’ (π β π
= (Scalarβπ)) |
81 | 80 | oveq1d 7420 |
. . . . . . 7
β’ (π β (π
RingHom π) = ((Scalarβπ) RingHom π)) |
82 | 79, 81 | eleqtrrd 2836 |
. . . . . 6
β’ (π β π΄ β (π
RingHom π)) |
83 | 71, 2 | rhm1 20259 |
. . . . . 6
β’ (π΄ β (π
RingHom π) β (π΄β(1rβπ
)) = (1rβπ)) |
84 | 82, 83 | syl 17 |
. . . . 5
β’ (π β (π΄β(1rβπ
)) = (1rβπ)) |
85 | 84 | fveq2d 6892 |
. . . 4
β’ (π β (πΈβ(π΄β(1rβπ
))) = (πΈβ(1rβπ))) |
86 | 71, 3 | rhm1 20259 |
. . . . 5
β’ (πΉ β (π
RingHom π) β (πΉβ(1rβπ
)) = (1rβπ)) |
87 | 33, 86 | syl 17 |
. . . 4
β’ (π β (πΉβ(1rβπ
)) = (1rβπ)) |
88 | 74, 85, 87 | 3eqtr3d 2780 |
. . 3
β’ (π β (πΈβ(1rβπ)) = (1rβπ)) |
89 | | eqid 2732 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
90 | | eqid 2732 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
91 | 11 | ringgrpd 20058 |
. . . . 5
β’ (π β π β Grp) |
92 | 13 | ringgrpd 20058 |
. . . . 5
β’ (π β π β Grp) |
93 | | eqid 2732 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
94 | | ringcmn 20092 |
. . . . . . . . 9
β’ (π β Ring β π β CMnd) |
95 | 13, 94 | syl 17 |
. . . . . . . 8
β’ (π β π β CMnd) |
96 | 95 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β π΅) β π β CMnd) |
97 | | ovex 7438 |
. . . . . . . . 9
β’
(β0 βm πΌ) β V |
98 | 17, 97 | rabex2 5333 |
. . . . . . . 8
β’ π· β V |
99 | 98 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π΅) β π· β V) |
100 | 6 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΌ β π) |
101 | 7 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π
β CRing) |
102 | 12 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β CRing) |
103 | 33 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΉ β (π
RingHom π)) |
104 | 35 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β πΊ:πΌβΆπΆ) |
105 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β π΅) |
106 | 9, 1, 26, 17, 27, 28, 5, 29, 30, 100, 101, 102, 103, 104, 105 | evlslem6 21635 |
. . . . . . . 8
β’ ((π β§ π β π΅) β ((π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ β§ (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ))) |
107 | 106 | simpld 495 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ) |
108 | 106 | simprd 496 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ)) |
109 | 26, 93, 96, 99, 107, 108 | gsumcl 19777 |
. . . . . 6
β’ ((π β§ π β π΅) β (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))))) β πΆ) |
110 | 109, 30 | fmptd 7110 |
. . . . 5
β’ (π β πΈ:π΅βΆπΆ) |
111 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπ
) = (+gβπ
) |
112 | | simplrl 775 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π₯ β π΅) |
113 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π¦ β π΅) |
114 | 9, 1, 111, 89, 112, 113 | mpladd 21559 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π₯(+gβπ)π¦) = (π₯ βf
(+gβπ
)π¦)) |
115 | 114 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((π₯(+gβπ)π¦)βπ) = ((π₯ βf
(+gβπ
)π¦)βπ)) |
116 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β π΅) |
117 | 9, 19, 1, 17, 116 | mplelf 21548 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯:π·βΆ(Baseβπ
)) |
118 | 117 | ffnd 6715 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ Fn π·) |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π₯ Fn π·) |
120 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β π΅) |
121 | 9, 19, 1, 17, 120 | mplelf 21548 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦:π·βΆ(Baseβπ
)) |
122 | 121 | ffnd 6715 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ Fn π·) |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π¦ Fn π·) |
124 | 98 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π· β V) |
125 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π β π·) |
126 | | fnfvof 7683 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ Fn π· β§ π¦ Fn π·) β§ (π· β V β§ π β π·)) β ((π₯ βf
(+gβπ
)π¦)βπ) = ((π₯βπ)(+gβπ
)(π¦βπ))) |
127 | 119, 123,
124, 125, 126 | syl22anc 837 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((π₯ βf
(+gβπ
)π¦)βπ) = ((π₯βπ)(+gβπ
)(π¦βπ))) |
128 | 115, 127 | eqtrd 2772 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((π₯(+gβπ)π¦)βπ) = ((π₯βπ)(+gβπ
)(π¦βπ))) |
129 | 128 | fveq2d 6892 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΉβ((π₯(+gβπ)π¦)βπ)) = (πΉβ((π₯βπ)(+gβπ
)(π¦βπ)))) |
130 | | rhmghm 20254 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (π
RingHom π) β πΉ β (π
GrpHom π)) |
131 | 33, 130 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β (π
GrpHom π)) |
132 | 131 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΉ β (π
GrpHom π)) |
133 | 117 | ffvelcdmda 7083 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π₯βπ) β (Baseβπ
)) |
134 | 121 | ffvelcdmda 7083 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π¦βπ) β (Baseβπ
)) |
135 | 19, 111, 90 | ghmlin 19091 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π
GrpHom π) β§ (π₯βπ) β (Baseβπ
) β§ (π¦βπ) β (Baseβπ
)) β (πΉβ((π₯βπ)(+gβπ
)(π¦βπ))) = ((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ)))) |
136 | 132, 133,
134, 135 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΉβ((π₯βπ)(+gβπ
)(π¦βπ))) = ((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ)))) |
137 | 129, 136 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΉβ((π₯(+gβπ)π¦)βπ)) = ((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ)))) |
138 | 137 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))) = (((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ))) Β· (π Ξ£g (π βf β πΊ)))) |
139 | 13 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π β Ring) |
140 | 64 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΉ:(Baseβπ
)βΆπΆ) |
141 | 140, 133 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΉβ(π₯βπ)) β πΆ) |
142 | 140, 134 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΉβ(π¦βπ)) β πΆ) |
143 | 56 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π β CMnd) |
144 | 35 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΊ:πΌβΆπΆ) |
145 | 17, 48, 28, 143, 125, 144 | psrbagev2 21631 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π Ξ£g (π βf β πΊ)) β πΆ) |
146 | 26, 90, 5 | ringdir 20075 |
. . . . . . . . . . . 12
β’ ((π β Ring β§ ((πΉβ(π₯βπ)) β πΆ β§ (πΉβ(π¦βπ)) β πΆ β§ (π Ξ£g (π βf β πΊ)) β πΆ)) β (((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ))) Β· (π Ξ£g (π βf β πΊ))) = (((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))(+gβπ)((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
147 | 139, 141,
142, 145, 146 | syl13anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (((πΉβ(π₯βπ))(+gβπ)(πΉβ(π¦βπ))) Β· (π Ξ£g (π βf β πΊ))) = (((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))(+gβπ)((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
148 | 138, 147 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))) = (((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))(+gβπ)((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
149 | 148 | mpteq2dva 5247 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ (((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))(+gβπ)((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
150 | 98 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π· β V) |
151 | | ovexd 7440 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ))) β V) |
152 | | ovexd 7440 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))) β V) |
153 | | eqidd 2733 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
154 | | eqidd 2733 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
155 | 150, 151,
152, 153, 154 | offval2 7686 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) βf
(+gβπ)(π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) = (π β π· β¦ (((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))(+gβπ)((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
156 | 149, 155 | eqtr4d 2775 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))) = ((π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) βf
(+gβπ)(π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
157 | 156 | oveq2d 7421 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))))) = (π Ξ£g ((π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) βf
(+gβπ)(π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))))) |
158 | 95 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β CMnd) |
159 | 6 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΌ β π) |
160 | 7 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π
β CRing) |
161 | 12 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β CRing) |
162 | 33 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΉ β (π
RingHom π)) |
163 | 35 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΊ:πΌβΆπΆ) |
164 | 9, 1, 26, 17, 27, 28, 5, 29, 30, 159, 160, 161, 162, 163, 116 | evlslem6 21635 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ β§ (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ))) |
165 | 164 | simpld 495 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ) |
166 | 9, 1, 26, 17, 27, 28, 5, 29, 30, 159, 160, 161, 162, 163, 120 | evlslem6 21635 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ β§ (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ))) |
167 | 166 | simpld 495 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ) |
168 | 164 | simprd 496 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ)) |
169 | 166 | simprd 496 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp
(0gβπ)) |
170 | 26, 93, 90, 158, 150, 165, 167, 168, 169 | gsumadd 19785 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g ((π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) βf
(+gβπ)(π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) = ((π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))(+gβπ)(π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))))) |
171 | 157, 170 | eqtrd 2772 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))))) = ((π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))(+gβπ)(π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))))) |
172 | 91 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Grp) |
173 | 1, 89 | grpcl 18823 |
. . . . . . . 8
β’ ((π β Grp β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπ)π¦) β π΅) |
174 | 172, 116,
120, 173 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ)π¦) β π΅) |
175 | | fveq1 6887 |
. . . . . . . . . . . 12
β’ (π = (π₯(+gβπ)π¦) β (πβπ) = ((π₯(+gβπ)π¦)βπ)) |
176 | 175 | fveq2d 6892 |
. . . . . . . . . . 11
β’ (π = (π₯(+gβπ)π¦) β (πΉβ(πβπ)) = (πΉβ((π₯(+gβπ)π¦)βπ))) |
177 | 176 | oveq1d 7420 |
. . . . . . . . . 10
β’ (π = (π₯(+gβπ)π¦) β ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))) = ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))) |
178 | 177 | mpteq2dv 5249 |
. . . . . . . . 9
β’ (π = (π₯(+gβπ)π¦) β (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
179 | 178 | oveq2d 7421 |
. . . . . . . 8
β’ (π = (π₯(+gβπ)π¦) β (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))))) = (π Ξ£g (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
180 | | ovex 7438 |
. . . . . . . 8
β’ (π Ξ£g
(π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ))))) β V |
181 | 179, 30, 180 | fvmpt 6995 |
. . . . . . 7
β’ ((π₯(+gβπ)π¦) β π΅ β (πΈβ(π₯(+gβπ)π¦)) = (π Ξ£g (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
182 | 174, 181 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(+gβπ)π¦)) = (π Ξ£g (π β π· β¦ ((πΉβ((π₯(+gβπ)π¦)βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
183 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = π₯ β (πβπ) = (π₯βπ)) |
184 | 183 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π = π₯ β (πΉβ(πβπ)) = (πΉβ(π₯βπ))) |
185 | 184 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π = π₯ β ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))) = ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))) |
186 | 185 | mpteq2dv 5249 |
. . . . . . . . . 10
β’ (π = π₯ β (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
187 | 186 | oveq2d 7421 |
. . . . . . . . 9
β’ (π = π₯ β (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))))) = (π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
188 | | ovex 7438 |
. . . . . . . . 9
β’ (π Ξ£g
(π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ))))) β V |
189 | 187, 30, 188 | fvmpt 6995 |
. . . . . . . 8
β’ (π₯ β π΅ β (πΈβπ₯) = (π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
190 | 116, 189 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ₯) = (π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
191 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (πβπ) = (π¦βπ)) |
192 | 191 | fveq2d 6892 |
. . . . . . . . . . . 12
β’ (π = π¦ β (πΉβ(πβπ)) = (πΉβ(π¦βπ))) |
193 | 192 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π = π¦ β ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))) = ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))) |
194 | 193 | mpteq2dv 5249 |
. . . . . . . . . 10
β’ (π = π¦ β (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) = (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) |
195 | 194 | oveq2d 7421 |
. . . . . . . . 9
β’ (π = π¦ β (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))))) = (π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
196 | | ovex 7438 |
. . . . . . . . 9
β’ (π Ξ£g
(π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))) β V |
197 | 195, 30, 196 | fvmpt 6995 |
. . . . . . . 8
β’ (π¦ β π΅ β (πΈβπ¦) = (π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
198 | 197 | ad2antll 727 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ¦) = (π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ)))))) |
199 | 190, 198 | oveq12d 7423 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πΈβπ₯)(+gβπ)(πΈβπ¦)) = ((π Ξ£g (π β π· β¦ ((πΉβ(π₯βπ)) Β· (π Ξ£g (π βf β πΊ)))))(+gβπ)(π Ξ£g (π β π· β¦ ((πΉβ(π¦βπ)) Β· (π Ξ£g (π βf β πΊ))))))) |
200 | 171, 182,
199 | 3eqtr4d 2782 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(+gβπ)π¦)) = ((πΈβπ₯)(+gβπ)(πΈβπ¦))) |
201 | 1, 26, 89, 90, 91, 92, 110, 200 | isghmd 19095 |
. . . 4
β’ (π β πΈ β (π GrpHom π)) |
202 | | eqid 2732 |
. . . . . . . . . . 11
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
203 | 202, 27 | rhmmhm 20250 |
. . . . . . . . . 10
β’ (πΉ β (π
RingHom π) β πΉ β ((mulGrpβπ
) MndHom π)) |
204 | 33, 203 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ β ((mulGrpβπ
) MndHom π)) |
205 | 204 | adantr 481 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β πΉ β ((mulGrpβπ
) MndHom π)) |
206 | | simprll 777 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π₯ β π΅) |
207 | 9, 19, 1, 17, 206 | mplelf 21548 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π₯:π·βΆ(Baseβπ
)) |
208 | | simprrl 779 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π§ β π·) |
209 | 207, 208 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π₯βπ§) β (Baseβπ
)) |
210 | | simprlr 778 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π¦ β π΅) |
211 | 9, 19, 1, 17, 210 | mplelf 21548 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π¦:π·βΆ(Baseβπ
)) |
212 | | simprrr 780 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π€ β π·) |
213 | 211, 212 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π¦βπ€) β (Baseβπ
)) |
214 | 202, 19 | mgpbas 19987 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβ(mulGrpβπ
)) |
215 | | eqid 2732 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
216 | 202, 215 | mgpplusg 19985 |
. . . . . . . . 9
β’
(.rβπ
) = (+gβ(mulGrpβπ
)) |
217 | 27, 5 | mgpplusg 19985 |
. . . . . . . . 9
β’ Β· =
(+gβπ) |
218 | 214, 216,
217 | mhmlin 18675 |
. . . . . . . 8
β’ ((πΉ β ((mulGrpβπ
) MndHom π) β§ (π₯βπ§) β (Baseβπ
) β§ (π¦βπ€) β (Baseβπ
)) β (πΉβ((π₯βπ§)(.rβπ
)(π¦βπ€))) = ((πΉβ(π₯βπ§)) Β· (πΉβ(π¦βπ€)))) |
219 | 205, 209,
213, 218 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΉβ((π₯βπ§)(.rβπ
)(π¦βπ€))) = ((πΉβ(π₯βπ§)) Β· (πΉβ(π¦βπ€)))) |
220 | 57 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β π β Mnd) |
221 | | simprl 769 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π§ β π·) |
222 | 17 | psrbagf 21462 |
. . . . . . . . . . . . . . 15
β’ (π§ β π· β π§:πΌβΆβ0) |
223 | 221, 222 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π§:πΌβΆβ0) |
224 | 223 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (π§βπ£) β
β0) |
225 | 17 | psrbagf 21462 |
. . . . . . . . . . . . . . 15
β’ (π€ β π· β π€:πΌβΆβ0) |
226 | 225 | ad2antll 727 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π€:πΌβΆβ0) |
227 | 226 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (π€βπ£) β
β0) |
228 | 35 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π· β§ π€ β π·)) β πΊ:πΌβΆπΆ) |
229 | 228 | ffvelcdmda 7083 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (πΊβπ£) β πΆ) |
230 | 48, 28, 217 | mulgnn0dir 18978 |
. . . . . . . . . . . . 13
β’ ((π β Mnd β§ ((π§βπ£) β β0 β§ (π€βπ£) β β0 β§ (πΊβπ£) β πΆ)) β (((π§βπ£) + (π€βπ£)) β (πΊβπ£)) = (((π§βπ£) β (πΊβπ£)) Β· ((π€βπ£) β (πΊβπ£)))) |
231 | 220, 224,
227, 229, 230 | syl13anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (((π§βπ£) + (π€βπ£)) β (πΊβπ£)) = (((π§βπ£) β (πΊβπ£)) Β· ((π€βπ£) β (πΊβπ£)))) |
232 | 231 | mpteq2dva 5247 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π£ β πΌ β¦ (((π§βπ£) + (π€βπ£)) β (πΊβπ£))) = (π£ β πΌ β¦ (((π§βπ£) β (πΊβπ£)) Β· ((π€βπ£) β (πΊβπ£))))) |
233 | 6 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β πΌ β π) |
234 | | ovexd 7440 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β ((π§βπ£) + (π€βπ£)) β V) |
235 | | fvexd 6903 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (πΊβπ£) β V) |
236 | 223 | ffnd 6715 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π§ Fn πΌ) |
237 | 226 | ffnd 6715 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π€ Fn πΌ) |
238 | | inidm 4217 |
. . . . . . . . . . . . 13
β’ (πΌ β© πΌ) = πΌ |
239 | | eqidd 2733 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (π§βπ£) = (π§βπ£)) |
240 | | eqidd 2733 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (π€βπ£) = (π€βπ£)) |
241 | 236, 237,
233, 233, 238, 239, 240 | offval 7675 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π§ βf + π€) = (π£ β πΌ β¦ ((π§βπ£) + (π€βπ£)))) |
242 | 35 | feqmptd 6957 |
. . . . . . . . . . . . 13
β’ (π β πΊ = (π£ β πΌ β¦ (πΊβπ£))) |
243 | 242 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β πΊ = (π£ β πΌ β¦ (πΊβπ£))) |
244 | 233, 234,
235, 241, 243 | offval2 7686 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π· β§ π€ β π·)) β ((π§ βf + π€) βf β πΊ) = (π£ β πΌ β¦ (((π§βπ£) + (π€βπ£)) β (πΊβπ£)))) |
245 | | ovexd 7440 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β ((π§βπ£) β (πΊβπ£)) β V) |
246 | | ovexd 7440 |
. . . . . . . . . . . 12
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β ((π€βπ£) β (πΊβπ£)) β V) |
247 | 35 | ffnd 6715 |
. . . . . . . . . . . . . 14
β’ (π β πΊ Fn πΌ) |
248 | 247 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ β π· β§ π€ β π·)) β πΊ Fn πΌ) |
249 | | eqidd 2733 |
. . . . . . . . . . . . 13
β’ (((π β§ (π§ β π· β§ π€ β π·)) β§ π£ β πΌ) β (πΊβπ£) = (πΊβπ£)) |
250 | 236, 248,
233, 233, 238, 239, 249 | offval 7675 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π§ βf β πΊ) = (π£ β πΌ β¦ ((π§βπ£) β (πΊβπ£)))) |
251 | 237, 248,
233, 233, 238, 240, 249 | offval 7675 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π€ βf β πΊ) = (π£ β πΌ β¦ ((π€βπ£) β (πΊβπ£)))) |
252 | 233, 245,
246, 250, 251 | offval2 7686 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π· β§ π€ β π·)) β ((π§ βf β πΊ) βf Β· (π€ βf β πΊ)) = (π£ β πΌ β¦ (((π§βπ£) β (πΊβπ£)) Β· ((π€βπ£) β (πΊβπ£))))) |
253 | 232, 244,
252 | 3eqtr4d 2782 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β ((π§ βf + π€) βf β πΊ) = ((π§ βf β πΊ) βf Β· (π€ βf β πΊ))) |
254 | 253 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π Ξ£g ((π§ βf + π€) βf β πΊ)) = (π Ξ£g ((π§ βf β πΊ) βf Β· (π€ βf β πΊ)))) |
255 | 56 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π β CMnd) |
256 | 17, 48, 28, 49, 255, 221, 228 | psrbagev1 21629 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π· β§ π€ β π·)) β ((π§ βf β πΊ):πΌβΆπΆ β§ (π§ βf β πΊ) finSupp (1rβπ))) |
257 | 256 | simpld 495 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π§ βf β πΊ):πΌβΆπΆ) |
258 | | simprr 771 |
. . . . . . . . . . . 12
β’ ((π β§ (π§ β π· β§ π€ β π·)) β π€ β π·) |
259 | 17, 48, 28, 49, 255, 258, 228 | psrbagev1 21629 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π· β§ π€ β π·)) β ((π€ βf β πΊ):πΌβΆπΆ β§ (π€ βf β πΊ) finSupp (1rβπ))) |
260 | 259 | simpld 495 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π€ βf β πΊ):πΌβΆπΆ) |
261 | 256 | simprd 496 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π§ βf β πΊ) finSupp (1rβπ)) |
262 | 259 | simprd 496 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π€ βf β πΊ) finSupp (1rβπ)) |
263 | 48, 49, 217, 255, 233, 257, 260, 261, 262 | gsumadd 19785 |
. . . . . . . . 9
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π Ξ£g ((π§ βf β πΊ) βf Β· (π€ βf β πΊ))) = ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ)))) |
264 | 254, 263 | eqtrd 2772 |
. . . . . . . 8
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π Ξ£g ((π§ βf + π€) βf β πΊ)) = ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ)))) |
265 | 264 | adantrl 714 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π Ξ£g ((π§ βf + π€) βf β πΊ)) = ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ)))) |
266 | 219, 265 | oveq12d 7423 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β ((πΉβ((π₯βπ§)(.rβπ
)(π¦βπ€))) Β· (π Ξ£g ((π§ βf + π€) βf β πΊ))) = (((πΉβ(π₯βπ§)) Β· (πΉβ(π¦βπ€))) Β· ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ))))) |
267 | 56 | adantr 481 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π β CMnd) |
268 | 64 | adantr 481 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β πΉ:(Baseβπ
)βΆπΆ) |
269 | 268, 209 | ffvelcdmd 7084 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΉβ(π₯βπ§)) β πΆ) |
270 | 268, 213 | ffvelcdmd 7084 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΉβ(π¦βπ€)) β πΆ) |
271 | 17, 48, 28, 255, 221, 228 | psrbagev2 21631 |
. . . . . . . 8
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π Ξ£g (π§ βf β πΊ)) β πΆ) |
272 | 271 | adantrl 714 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π Ξ£g (π§ βf β πΊ)) β πΆ) |
273 | 17, 48, 28, 255, 258, 228 | psrbagev2 21631 |
. . . . . . . 8
β’ ((π β§ (π§ β π· β§ π€ β π·)) β (π Ξ£g (π€ βf β πΊ)) β πΆ) |
274 | 273 | adantrl 714 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π Ξ£g (π€ βf β πΊ)) β πΆ) |
275 | 48, 217 | cmn4 19663 |
. . . . . . 7
β’ ((π β CMnd β§ ((πΉβ(π₯βπ§)) β πΆ β§ (πΉβ(π¦βπ€)) β πΆ) β§ ((π Ξ£g (π§ βf β πΊ)) β πΆ β§ (π Ξ£g (π€ βf β πΊ)) β πΆ)) β (((πΉβ(π₯βπ§)) Β· (πΉβ(π¦βπ€))) Β· ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ)))) = (((πΉβ(π₯βπ§)) Β· (π Ξ£g (π§ βf β πΊ))) Β· ((πΉβ(π¦βπ€)) Β· (π Ξ£g (π€ βf β πΊ))))) |
276 | 267, 269,
270, 272, 274, 275 | syl122anc 1379 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (((πΉβ(π₯βπ§)) Β· (πΉβ(π¦βπ€))) Β· ((π Ξ£g (π§ βf β πΊ)) Β· (π Ξ£g (π€ βf β πΊ)))) = (((πΉβ(π₯βπ§)) Β· (π Ξ£g (π§ βf β πΊ))) Β· ((πΉβ(π¦βπ€)) Β· (π Ξ£g (π€ βf β πΊ))))) |
277 | 266, 276 | eqtrd 2772 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β ((πΉβ((π₯βπ§)(.rβπ
)(π¦βπ€))) Β· (π Ξ£g ((π§ βf + π€) βf β πΊ))) = (((πΉβ(π₯βπ§)) Β· (π Ξ£g (π§ βf β πΊ))) Β· ((πΉβ(π¦βπ€)) Β· (π Ξ£g (π€ βf β πΊ))))) |
278 | 6 | adantr 481 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β πΌ β π) |
279 | 7 | adantr 481 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π
β CRing) |
280 | 12 | adantr 481 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π β CRing) |
281 | 33 | adantr 481 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β πΉ β (π
RingHom π)) |
282 | 35 | adantr 481 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β πΊ:πΌβΆπΆ) |
283 | 17 | psrbagaddcl 21472 |
. . . . . . 7
β’ ((π§ β π· β§ π€ β π·) β (π§ βf + π€) β π·) |
284 | 283 | ad2antll 727 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (π§ βf + π€) β π·) |
285 | 8 | adantr 481 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β π
β Ring) |
286 | 19, 215 | ringcl 20066 |
. . . . . . 7
β’ ((π
β Ring β§ (π₯βπ§) β (Baseβπ
) β§ (π¦βπ€) β (Baseβπ
)) β ((π₯βπ§)(.rβπ
)(π¦βπ€)) β (Baseβπ
)) |
287 | 285, 209,
213, 286 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β ((π₯βπ§)(.rβπ
)(π¦βπ€)) β (Baseβπ
)) |
288 | 9, 1, 26, 19, 17, 27, 28, 5, 29, 30, 278, 279, 280, 281, 282, 18, 284, 287 | evlslem3 21634 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΈβ(π£ β π· β¦ if(π£ = (π§ βf + π€), ((π₯βπ§)(.rβπ
)(π¦βπ€)), (0gβπ
)))) = ((πΉβ((π₯βπ§)(.rβπ
)(π¦βπ€))) Β· (π Ξ£g ((π§ βf + π€) βf β πΊ)))) |
289 | 9, 1, 26, 19, 17, 27, 28, 5, 29, 30, 278, 279, 280, 281, 282, 18, 208, 209 | evlslem3 21634 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΈβ(π£ β π· β¦ if(π£ = π§, (π₯βπ§), (0gβπ
)))) = ((πΉβ(π₯βπ§)) Β· (π Ξ£g (π§ βf β πΊ)))) |
290 | 9, 1, 26, 19, 17, 27, 28, 5, 29, 30, 278, 279, 280, 281, 282, 18, 212, 213 | evlslem3 21634 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΈβ(π£ β π· β¦ if(π£ = π€, (π¦βπ€), (0gβπ
)))) = ((πΉβ(π¦βπ€)) Β· (π Ξ£g (π€ βf β πΊ)))) |
291 | 289, 290 | oveq12d 7423 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β ((πΈβ(π£ β π· β¦ if(π£ = π§, (π₯βπ§), (0gβπ
)))) Β· (πΈβ(π£ β π· β¦ if(π£ = π€, (π¦βπ€), (0gβπ
))))) = (((πΉβ(π₯βπ§)) Β· (π Ξ£g (π§ βf β πΊ))) Β· ((πΉβ(π¦βπ€)) Β· (π Ξ£g (π€ βf β πΊ))))) |
292 | 277, 288,
291 | 3eqtr4d 2782 |
. . . 4
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π§ β π· β§ π€ β π·))) β (πΈβ(π£ β π· β¦ if(π£ = (π§ βf + π€), ((π₯βπ§)(.rβπ
)(π¦βπ€)), (0gβπ
)))) = ((πΈβ(π£ β π· β¦ if(π£ = π§, (π₯βπ§), (0gβπ
)))) Β· (πΈβ(π£ β π· β¦ if(π£ = π€, (π¦βπ€), (0gβπ
)))))) |
293 | 9, 1, 5, 18, 17, 6, 7, 12, 201, 292 | evlslem2 21633 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(.rβπ)π¦)) = ((πΈβπ₯) Β· (πΈβπ¦))) |
294 | 1, 2, 3, 4, 5, 11,
13, 88, 293, 26, 89, 90, 110, 200 | isrhmd 20258 |
. 2
β’ (π β πΈ β (π RingHom π)) |
295 | | ovex 7438 |
. . . . . 6
β’ (π Ξ£g
(π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ))))) β V |
296 | 295, 30 | fnmpti 6690 |
. . . . 5
β’ πΈ Fn π΅ |
297 | 296 | a1i 11 |
. . . 4
β’ (π β πΈ Fn π΅) |
298 | 19, 1 | rhmf 20255 |
. . . . . 6
β’ (π΄ β (π
RingHom π) β π΄:(Baseβπ
)βΆπ΅) |
299 | 82, 298 | syl 17 |
. . . . 5
β’ (π β π΄:(Baseβπ
)βΆπ΅) |
300 | 299 | ffnd 6715 |
. . . 4
β’ (π β π΄ Fn (Baseβπ
)) |
301 | 299 | frnd 6722 |
. . . 4
β’ (π β ran π΄ β π΅) |
302 | | fnco 6664 |
. . . 4
β’ ((πΈ Fn π΅ β§ π΄ Fn (Baseβπ
) β§ ran π΄ β π΅) β (πΈ β π΄) Fn (Baseβπ
)) |
303 | 297, 300,
301, 302 | syl3anc 1371 |
. . 3
β’ (π β (πΈ β π΄) Fn (Baseβπ
)) |
304 | 64 | ffnd 6715 |
. . 3
β’ (π β πΉ Fn (Baseβπ
)) |
305 | | fvco2 6985 |
. . . . 5
β’ ((π΄ Fn (Baseβπ
) β§ π₯ β (Baseβπ
)) β ((πΈ β π΄)βπ₯) = (πΈβ(π΄βπ₯))) |
306 | 300, 305 | sylan 580 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΈ β π΄)βπ₯) = (πΈβ(π΄βπ₯))) |
307 | 306, 69 | eqtrd 2772 |
. . 3
β’ ((π β§ π₯ β (Baseβπ
)) β ((πΈ β π΄)βπ₯) = (πΉβπ₯)) |
308 | 303, 304,
307 | eqfnfvd 7032 |
. 2
β’ (π β (πΈ β π΄) = πΉ) |
309 | 9, 29, 1, 6, 8 | mvrf2 21543 |
. . . . 5
β’ (π β π:πΌβΆπ΅) |
310 | 309 | ffnd 6715 |
. . . 4
β’ (π β π Fn πΌ) |
311 | 309 | frnd 6722 |
. . . 4
β’ (π β ran π β π΅) |
312 | | fnco 6664 |
. . . 4
β’ ((πΈ Fn π΅ β§ π Fn πΌ β§ ran π β π΅) β (πΈ β π) Fn πΌ) |
313 | 297, 310,
311, 312 | syl3anc 1371 |
. . 3
β’ (π β (πΈ β π) Fn πΌ) |
314 | | fvco2 6985 |
. . . . 5
β’ ((π Fn πΌ β§ π₯ β πΌ) β ((πΈ β π)βπ₯) = (πΈβ(πβπ₯))) |
315 | 310, 314 | sylan 580 |
. . . 4
β’ ((π β§ π₯ β πΌ) β ((πΈ β π)βπ₯) = (πΈβ(πβπ₯))) |
316 | 6 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β πΌ β π) |
317 | 7 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π
β CRing) |
318 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
319 | 29, 17, 18, 71, 316, 317, 318 | mvrval 21532 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (πβπ₯) = (π¦ β π· β¦ if(π¦ = (π§ β πΌ β¦ if(π§ = π₯, 1, 0)), (1rβπ
), (0gβπ
)))) |
320 | 319 | fveq2d 6892 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πΈβ(πβπ₯)) = (πΈβ(π¦ β π· β¦ if(π¦ = (π§ β πΌ β¦ if(π§ = π₯, 1, 0)), (1rβπ
), (0gβπ
))))) |
321 | 12 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β π β CRing) |
322 | 33 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β πΉ β (π
RingHom π)) |
323 | 35 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β πΊ:πΌβΆπΆ) |
324 | 17 | psrbagsn 21615 |
. . . . . . . 8
β’ (πΌ β π β (π§ β πΌ β¦ if(π§ = π₯, 1, 0)) β π·) |
325 | 6, 324 | syl 17 |
. . . . . . 7
β’ (π β (π§ β πΌ β¦ if(π§ = π₯, 1, 0)) β π·) |
326 | 325 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (π§ β πΌ β¦ if(π§ = π₯, 1, 0)) β π·) |
327 | 73 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (1rβπ
) β (Baseβπ
)) |
328 | 9, 1, 26, 19, 17, 27, 28, 5, 29, 30, 316, 317, 321, 322, 323, 18, 326, 327 | evlslem3 21634 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (πΈβ(π¦ β π· β¦ if(π¦ = (π§ β πΌ β¦ if(π§ = π₯, 1, 0)), (1rβπ
), (0gβπ
)))) = ((πΉβ(1rβπ
)) Β· (π Ξ£g ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ)))) |
329 | 87 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (πΉβ(1rβπ
)) = (1rβπ)) |
330 | | 1nn0 12484 |
. . . . . . . . . . . . . 14
β’ 1 β
β0 |
331 | | 0nn0 12483 |
. . . . . . . . . . . . . 14
β’ 0 β
β0 |
332 | 330, 331 | ifcli 4574 |
. . . . . . . . . . . . 13
β’ if(π§ = π₯, 1, 0) β
β0 |
333 | 332 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β πΌ) β if(π§ = π₯, 1, 0) β
β0) |
334 | 35 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β πΌ) β (πΊβπ§) β πΆ) |
335 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ (π β (π§ β πΌ β¦ if(π§ = π₯, 1, 0)) = (π§ β πΌ β¦ if(π§ = π₯, 1, 0))) |
336 | 35 | feqmptd 6957 |
. . . . . . . . . . . 12
β’ (π β πΊ = (π§ β πΌ β¦ (πΊβπ§))) |
337 | 6, 333, 334, 335, 336 | offval2 7686 |
. . . . . . . . . . 11
β’ (π β ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ) = (π§ β πΌ β¦ (if(π§ = π₯, 1, 0) β (πΊβπ§)))) |
338 | | oveq1 7412 |
. . . . . . . . . . . . . 14
β’ (1 =
if(π§ = π₯, 1, 0) β (1 β (πΊβπ§)) = (if(π§ = π₯, 1, 0) β (πΊβπ§))) |
339 | 338 | eqeq1d 2734 |
. . . . . . . . . . . . 13
β’ (1 =
if(π§ = π₯, 1, 0) β ((1 β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ)) β (if(π§ = π₯, 1, 0) β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ)))) |
340 | | oveq1 7412 |
. . . . . . . . . . . . . 14
β’ (0 =
if(π§ = π₯, 1, 0) β (0 β (πΊβπ§)) = (if(π§ = π₯, 1, 0) β (πΊβπ§))) |
341 | 340 | eqeq1d 2734 |
. . . . . . . . . . . . 13
β’ (0 =
if(π§ = π₯, 1, 0) β ((0 β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ)) β (if(π§ = π₯, 1, 0) β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ)))) |
342 | 334 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β πΌ) β§ π§ = π₯) β (πΊβπ§) β πΆ) |
343 | 48, 28 | mulg1 18955 |
. . . . . . . . . . . . . . 15
β’ ((πΊβπ§) β πΆ β (1 β (πΊβπ§)) = (πΊβπ§)) |
344 | 342, 343 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΌ) β§ π§ = π₯) β (1 β (πΊβπ§)) = (πΊβπ§)) |
345 | | iftrue 4533 |
. . . . . . . . . . . . . . 15
β’ (π§ = π₯ β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (πΊβπ§)) |
346 | 345 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΌ) β§ π§ = π₯) β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (πΊβπ§)) |
347 | 344, 346 | eqtr4d 2775 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β πΌ) β§ π§ = π₯) β (1 β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ))) |
348 | 48, 49, 28 | mulg0 18951 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπ§) β πΆ β (0 β (πΊβπ§)) = (1rβπ)) |
349 | 334, 348 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β πΌ) β (0 β (πΊβπ§)) = (1rβπ)) |
350 | 349 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΌ) β§ Β¬ π§ = π₯) β (0 β (πΊβπ§)) = (1rβπ)) |
351 | | iffalse 4536 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π§ = π₯ β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (1rβπ)) |
352 | 351 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β πΌ) β§ Β¬ π§ = π₯) β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (1rβπ)) |
353 | 350, 352 | eqtr4d 2775 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β πΌ) β§ Β¬ π§ = π₯) β (0 β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ))) |
354 | 339, 341,
347, 353 | ifbothda 4565 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β πΌ) β (if(π§ = π₯, 1, 0) β (πΊβπ§)) = if(π§ = π₯, (πΊβπ§), (1rβπ))) |
355 | 354 | mpteq2dva 5247 |
. . . . . . . . . . 11
β’ (π β (π§ β πΌ β¦ (if(π§ = π₯, 1, 0) β (πΊβπ§))) = (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))) |
356 | 337, 355 | eqtrd 2772 |
. . . . . . . . . 10
β’ (π β ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ) = (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))) |
357 | 356 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ) = (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))) |
358 | 357 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β (π Ξ£g ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ)) = (π Ξ£g (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ))))) |
359 | 57 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β π β Mnd) |
360 | 334 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΌ) β§ π§ β πΌ) β (πΊβπ§) β πΆ) |
361 | 26, 3 | ringidcl 20076 |
. . . . . . . . . . . . 13
β’ (π β Ring β
(1rβπ)
β πΆ) |
362 | 13, 361 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (1rβπ) β πΆ) |
363 | 362 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΌ) β§ π§ β πΌ) β (1rβπ) β πΆ) |
364 | 360, 363 | ifcld 4573 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΌ) β§ π§ β πΌ) β if(π§ = π₯, (πΊβπ§), (1rβπ)) β πΆ) |
365 | 364 | fmpttd 7111 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ))):πΌβΆπΆ) |
366 | | eldifsnneq 4793 |
. . . . . . . . . . . 12
β’ (π§ β (πΌ β {π₯}) β Β¬ π§ = π₯) |
367 | 366, 351 | syl 17 |
. . . . . . . . . . 11
β’ (π§ β (πΌ β {π₯}) β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (1rβπ)) |
368 | 367 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΌ) β§ π§ β (πΌ β {π₯})) β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (1rβπ)) |
369 | 368, 316 | suppss2 8181 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β ((π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ))) supp (1rβπ)) β {π₯}) |
370 | 48, 49, 359, 316, 318, 365, 369 | gsumpt 19824 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β (π Ξ£g (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))) = ((π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))βπ₯)) |
371 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π§ = π₯ β (πΊβπ§) = (πΊβπ₯)) |
372 | 345, 371 | eqtrd 2772 |
. . . . . . . . . 10
β’ (π§ = π₯ β if(π§ = π₯, (πΊβπ§), (1rβπ)) = (πΊβπ₯)) |
373 | | eqid 2732 |
. . . . . . . . . 10
β’ (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ))) = (π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ))) |
374 | | fvex 6901 |
. . . . . . . . . 10
β’ (πΊβπ₯) β V |
375 | 372, 373,
374 | fvmpt 6995 |
. . . . . . . . 9
β’ (π₯ β πΌ β ((π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))βπ₯) = (πΊβπ₯)) |
376 | 375 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β ((π§ β πΌ β¦ if(π§ = π₯, (πΊβπ§), (1rβπ)))βπ₯) = (πΊβπ₯)) |
377 | 358, 370,
376 | 3eqtrd 2776 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (π Ξ£g ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ)) = (πΊβπ₯)) |
378 | 329, 377 | oveq12d 7423 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β ((πΉβ(1rβπ
)) Β· (π Ξ£g ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ))) =
((1rβπ)
Β·
(πΊβπ₯))) |
379 | 26, 5, 3 | ringlidm 20079 |
. . . . . . 7
β’ ((π β Ring β§ (πΊβπ₯) β πΆ) β ((1rβπ) Β· (πΊβπ₯)) = (πΊβπ₯)) |
380 | 13, 47, 379 | syl2an2r 683 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β ((1rβπ) Β· (πΊβπ₯)) = (πΊβπ₯)) |
381 | 378, 380 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β ((πΉβ(1rβπ
)) Β· (π Ξ£g ((π§ β πΌ β¦ if(π§ = π₯, 1, 0)) βf β πΊ))) = (πΊβπ₯)) |
382 | 320, 328,
381 | 3eqtrd 2776 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (πΈβ(πβπ₯)) = (πΊβπ₯)) |
383 | 315, 382 | eqtrd 2772 |
. . 3
β’ ((π β§ π₯ β πΌ) β ((πΈ β π)βπ₯) = (πΊβπ₯)) |
384 | 313, 247,
383 | eqfnfvd 7032 |
. 2
β’ (π β (πΈ β π) = πΊ) |
385 | 294, 308,
384 | 3jca 1128 |
1
β’ (π β (πΈ β (π RingHom π) β§ (πΈ β π΄) = πΉ β§ (πΈ β π) = πΊ)) |