Step | Hyp | Ref
| Expression |
1 | | evlslem2.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
2 | | eqid 2730 |
. . . . 5
โข
(.rโ๐) = (.rโ๐) |
3 | | eqid 2730 |
. . . . 5
โข
(0gโ๐) = (0gโ๐) |
4 | | evlslem2.d |
. . . . . . 7
โข ๐ท = {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} |
5 | | ovex 7444 |
. . . . . . 7
โข
(โ0 โm ๐ผ) โ V |
6 | 4, 5 | rabex2 5333 |
. . . . . 6
โข ๐ท โ V |
7 | 6 | a1i 11 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ท โ V) |
8 | | evlslem2.i |
. . . . . . 7
โข (๐ โ ๐ผ โ ๐) |
9 | | evlslem2.r |
. . . . . . . 8
โข (๐ โ ๐
โ CRing) |
10 | | crngring 20139 |
. . . . . . . 8
โข (๐
โ CRing โ ๐
โ Ring) |
11 | 9, 10 | syl 17 |
. . . . . . 7
โข (๐ โ ๐
โ Ring) |
12 | | evlslem2.p |
. . . . . . . 8
โข ๐ = (๐ผ mPoly ๐
) |
13 | 12 | mplring 21797 |
. . . . . . 7
โข ((๐ผ โ ๐ โง ๐
โ Ring) โ ๐ โ Ring) |
14 | 8, 11, 13 | syl2anc 582 |
. . . . . 6
โข (๐ โ ๐ โ Ring) |
15 | 14 | adantr 479 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Ring) |
16 | | evlslem2.z |
. . . . . 6
โข 0 =
(0gโ๐
) |
17 | | eqid 2730 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ๐
) |
18 | 8 | ad2antrr 722 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ผ โ ๐) |
19 | 11 | ad2antrr 722 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐
โ Ring) |
20 | | simprl 767 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฅ โ ๐ต) |
21 | 12, 17, 1, 4, 20 | mplelf 21776 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฅ:๐ทโถ(Baseโ๐
)) |
22 | 21 | ffvelcdmda 7085 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ฅโ๐) โ (Baseโ๐
)) |
23 | | simpr 483 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ โ ๐ท) |
24 | 12, 4, 16, 17, 18, 19, 1, 22, 23 | mplmon2cl 21848 |
. . . . 5
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ ๐ต) |
25 | 8 | ad2antrr 722 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ผ โ ๐) |
26 | 11 | ad2antrr 722 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐
โ Ring) |
27 | | simprr 769 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฆ โ ๐ต) |
28 | 12, 17, 1, 4, 27 | mplelf 21776 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฆ:๐ทโถ(Baseโ๐
)) |
29 | 28 | ffvelcdmda 7085 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ฆโ๐) โ (Baseโ๐
)) |
30 | | simpr 483 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ โ ๐ท) |
31 | 12, 4, 16, 17, 25, 26, 1, 29, 30 | mplmon2cl 21848 |
. . . . 5
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ ๐ต) |
32 | 6 | mptex 7226 |
. . . . . . . . . . . 12
โข (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ
V |
33 | | funmpt 6585 |
. . . . . . . . . . . 12
โข Fun
(๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) |
34 | | fvex 6903 |
. . . . . . . . . . . 12
โข
(0gโ๐) โ V |
35 | 32, 33, 34 | 3pm3.2i 1337 |
. . . . . . . . . . 11
โข ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โง
(0gโ๐)
โ V) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โง
(0gโ๐)
โ V)) |
37 | | simpr 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ฆ โ ๐ต) |
38 | 9 | adantr 479 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐
โ CRing) |
39 | 12, 1, 16, 37, 38 | mplelsfi 21773 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ฆ finSupp 0 ) |
40 | 39 | fsuppimpd 9371 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ต) โ (๐ฆ supp 0 ) โ
Fin) |
41 | 12, 17, 1, 4, 37 | mplelf 21776 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ฆ:๐ทโถ(Baseโ๐
)) |
42 | | ssidd 4004 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ ๐ต) โ (๐ฆ supp 0 ) โ (๐ฆ supp 0 )) |
43 | 6 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ ๐ต) โ ๐ท โ V) |
44 | 16 | fvexi 6904 |
. . . . . . . . . . . . . . . . 17
โข 0 โ
V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ ๐ต) โ 0 โ V) |
46 | 41, 42, 43, 45 | suppssr 8183 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ (๐ฆโ๐) = 0 ) |
47 | 46 | ifeq1d 4546 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ if(๐ = ๐, (๐ฆโ๐), 0 ) = if(๐ = ๐, 0 , 0 )) |
48 | | ifid 4567 |
. . . . . . . . . . . . . 14
โข if(๐ = ๐, 0 , 0 ) = 0 |
49 | 47, 48 | eqtrdi 2786 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ if(๐ = ๐, (๐ฆโ๐), 0 ) = 0 ) |
50 | 49 | mpteq2dv 5249 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) = (๐ โ ๐ท โฆ 0 )) |
51 | | ringgrp 20132 |
. . . . . . . . . . . . . . . 16
โข (๐
โ Ring โ ๐
โ Grp) |
52 | 11, 51 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐
โ Grp) |
53 | 12, 4, 16, 3, 8, 52 | mpl0 21784 |
. . . . . . . . . . . . . 14
โข (๐ โ (0gโ๐) = (๐ท ร { 0 })) |
54 | | fconstmpt 5737 |
. . . . . . . . . . . . . 14
โข (๐ท ร { 0 }) = (๐ โ ๐ท โฆ 0 ) |
55 | 53, 54 | eqtrdi 2786 |
. . . . . . . . . . . . 13
โข (๐ โ (0gโ๐) = (๐ โ ๐ท โฆ 0 )) |
56 | 55 | ad2antrr 722 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ
(0gโ๐) =
(๐ โ ๐ท โฆ 0 )) |
57 | 50, 56 | eqtr4d 2773 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ โ (๐ท โ (๐ฆ supp 0 ))) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) =
(0gโ๐)) |
58 | 57, 43 | suppss2 8187 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ต) โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ (๐ฆ supp 0
)) |
59 | | suppssfifsupp 9380 |
. . . . . . . . . 10
โข ((((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โง
(0gโ๐)
โ V) โง ((๐ฆ supp
0 )
โ Fin โง ((๐ โ
๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ (๐ฆ supp 0 ))) โ
(๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)) |
60 | 36, 40, 58, 59 | syl12anc 833 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ต) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)) |
61 | 60 | ralrimiva 3144 |
. . . . . . . 8
โข (๐ โ โ๐ฆ โ ๐ต (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)) |
62 | | fveq1 6889 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ฅ โ (๐ฆโ๐) = (๐ฅโ๐)) |
63 | 62 | ifeq1d 4546 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ฅ โ if(๐ = ๐, (๐ฆโ๐), 0 ) = if(๐ = ๐, (๐ฅโ๐), 0 )) |
64 | 63 | mpteq2dv 5249 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ฅ โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) = (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) |
65 | 64 | mpteq2dv 5249 |
. . . . . . . . . 10
โข (๐ฆ = ๐ฅ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) = (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) |
66 | 65 | breq1d 5157 |
. . . . . . . . 9
โข (๐ฆ = ๐ฅ โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)
โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) finSupp
(0gโ๐))) |
67 | 66 | cbvralvw 3232 |
. . . . . . . 8
โข
(โ๐ฆ โ
๐ต (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)
โ โ๐ฅ โ
๐ต (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) finSupp
(0gโ๐)) |
68 | 61, 67 | sylib 217 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ ๐ต (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) finSupp
(0gโ๐)) |
69 | 68 | r19.21bi 3246 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ต) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) finSupp
(0gโ๐)) |
70 | 69 | adantrr 713 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) finSupp
(0gโ๐)) |
71 | | equequ2 2027 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ = ๐ โ ๐ = ๐)) |
72 | | fveq2 6890 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ฆโ๐) = (๐ฆโ๐)) |
73 | 71, 72 | ifbieq1d 4551 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ = ๐, (๐ฆโ๐), 0 ) = if(๐ = ๐, (๐ฆโ๐), 0 )) |
74 | 73 | mpteq2dv 5249 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) = (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) |
75 | 74 | cbvmptv 5260 |
. . . . . 6
โข (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) = (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) |
76 | 60 | adantrl 712 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)) |
77 | 75, 76 | eqbrtrid 5182 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) finSupp
(0gโ๐)) |
78 | 1, 2, 3, 7, 7, 15,
24, 31, 70, 77 | gsumdixp 20207 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))))(.rโ๐)(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) = (๐ ฮฃg (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
79 | 78 | fveq2d 6894 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))))(.rโ๐)(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
80 | | ringcmn 20170 |
. . . . . 6
โข (๐ โ Ring โ ๐ โ CMnd) |
81 | 14, 80 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ CMnd) |
82 | 81 | adantr 479 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ CMnd) |
83 | | evlslem2.s |
. . . . . . 7
โข (๐ โ ๐ โ CRing) |
84 | | crngring 20139 |
. . . . . . 7
โข (๐ โ CRing โ ๐ โ Ring) |
85 | 83, 84 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ Ring) |
86 | 85 | adantr 479 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Ring) |
87 | | ringmnd 20137 |
. . . . 5
โข (๐ โ Ring โ ๐ โ Mnd) |
88 | 86, 87 | syl 17 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Mnd) |
89 | 6, 6 | xpex 7742 |
. . . . 5
โข (๐ท ร ๐ท) โ V |
90 | 89 | a1i 11 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ท ร ๐ท) โ V) |
91 | | evlslem2.e1 |
. . . . . 6
โข (๐ โ ๐ธ โ (๐ GrpHom ๐)) |
92 | | ghmmhm 19140 |
. . . . . 6
โข (๐ธ โ (๐ GrpHom ๐) โ ๐ธ โ (๐ MndHom ๐)) |
93 | 91, 92 | syl 17 |
. . . . 5
โข (๐ โ ๐ธ โ (๐ MndHom ๐)) |
94 | 93 | adantr 479 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ธ โ (๐ MndHom ๐)) |
95 | 14 | ad2antrr 722 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ Ring) |
96 | 24 | adantrr 713 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ ๐ต) |
97 | 31 | adantrl 712 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ ๐ต) |
98 | 1, 2 | ringcl 20144 |
. . . . . . 7
โข ((๐ โ Ring โง (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ ๐ต โง (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ ๐ต) โ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ ๐ต) |
99 | 95, 96, 97, 98 | syl3anc 1369 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ ๐ต) |
100 | 99 | ralrimivva 3198 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ๐ โ ๐ท โ๐ โ ๐ท ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ ๐ต) |
101 | | eqid 2730 |
. . . . . 6
โข (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) |
102 | 101 | fmpo 8056 |
. . . . 5
โข
(โ๐ โ
๐ท โ๐ โ ๐ท ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ ๐ต โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))):(๐ท ร ๐ท)โถ๐ต) |
103 | 100, 102 | sylib 217 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))):(๐ท ร ๐ท)โถ๐ต) |
104 | 6, 6 | mpoex 8068 |
. . . . . . 7
โข (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ
V |
105 | 101 | mpofun 7534 |
. . . . . . 7
โข Fun
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) |
106 | 104, 105,
34 | 3pm3.2i 1337 |
. . . . . 6
โข ((๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V) |
107 | 106 | a1i 11 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V)) |
108 | 70 | fsuppimpd 9371 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
โ Fin) |
109 | 77 | fsuppimpd 9371 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ Fin) |
110 | | xpfi 9319 |
. . . . . 6
โข ((((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
โ Fin โง ((๐ โ
๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ Fin) โ (((๐
โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
ร ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐)))
โ Fin) |
111 | 108, 109,
110 | syl2anc 582 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
ร ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐)))
โ Fin) |
112 | 1, 3, 2, 15, 24, 31, 7, 7 | evlslem4 21856 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) supp
(0gโ๐))
โ (((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
ร ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐)))) |
113 | | suppssfifsupp 9380 |
. . . . 5
โข ((((๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V) โง ((((๐
โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
ร ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐)))
โ Fin โง ((๐ โ
๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) supp
(0gโ๐))
โ (((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
ร ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐)))))
โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) finSupp
(0gโ๐)) |
114 | 107, 111,
112, 113 | syl12anc 833 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) finSupp
(0gโ๐)) |
115 | 1, 3, 82, 88, 90, 94, 103, 114 | gsummhm 19847 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
116 | 8 | ad2antrr 722 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ผ โ ๐) |
117 | 9 | ad2antrr 722 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐
โ CRing) |
118 | | eqid 2730 |
. . . . . . . . . 10
โข
(.rโ๐
) = (.rโ๐
) |
119 | | simprl 767 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ ๐ท) |
120 | | simprr 769 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ๐ โ ๐ท) |
121 | 22 | adantrr 713 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ฅโ๐) โ (Baseโ๐
)) |
122 | 29 | adantrl 712 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ฆโ๐) โ (Baseโ๐
)) |
123 | 12, 4, 16, 17, 116, 117, 2, 118, 119, 120, 121, 122 | mplmon2mul 21849 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) = (๐ โ ๐ท โฆ if(๐ = (๐ โf + ๐), ((๐ฅโ๐)(.rโ๐
)(๐ฆโ๐)), 0 ))) |
124 | 123 | fveq2d 6894 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = (๐ธโ(๐ โ ๐ท โฆ if(๐ = (๐ โf + ๐), ((๐ฅโ๐)(.rโ๐
)(๐ฆโ๐)), 0 )))) |
125 | | evlslem2.e2 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง (๐ โ ๐ท โง ๐ โ ๐ท))) โ (๐ธโ(๐ โ ๐ท โฆ if(๐ = (๐ โf + ๐), ((๐ฅโ๐)(.rโ๐
)(๐ฆโ๐)), 0 ))) = ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
126 | 125 | anassrs 466 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ธโ(๐ โ ๐ท โฆ if(๐ = (๐ โf + ๐), ((๐ฅโ๐)(.rโ๐
)(๐ฆโ๐)), 0 ))) = ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
127 | 124, 126 | eqtrd 2770 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
128 | 127 | 3impb 1113 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท โง ๐ โ ๐ท) โ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
129 | 128 | mpoeq3dva 7488 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท, ๐ โ ๐ท โฆ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) = (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
130 | 129 | oveq2d 7427 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ ๐ท, ๐ โ ๐ท โฆ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ ฮฃg
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
131 | | eqidd 2731 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
132 | | eqid 2730 |
. . . . . . . . . 10
โข
(Baseโ๐) =
(Baseโ๐) |
133 | 1, 132 | ghmf 19134 |
. . . . . . . . 9
โข (๐ธ โ (๐ GrpHom ๐) โ ๐ธ:๐ตโถ(Baseโ๐)) |
134 | 91, 133 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ธ:๐ตโถ(Baseโ๐)) |
135 | 134 | feqmptd 6959 |
. . . . . . 7
โข (๐ โ ๐ธ = (๐ง โ ๐ต โฆ (๐ธโ๐ง))) |
136 | 135 | adantr 479 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ธ = (๐ง โ ๐ต โฆ (๐ธโ๐ง))) |
137 | | fveq2 6890 |
. . . . . 6
โข (๐ง = ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ (๐ธโ๐ง) = (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
138 | 99, 131, 136, 137 | fmpoco 8083 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธ โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) = (๐ โ ๐ท, ๐ โ ๐ท โฆ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
139 | 138 | oveq2d 7427 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ ฮฃg
(๐ โ ๐ท, ๐ โ ๐ท โฆ (๐ธโ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
140 | | eqidd 2731 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) = (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) |
141 | | fveq2 6890 |
. . . . . . . 8
โข (๐ง = (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ (๐ธโ๐ง) = (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) |
142 | 24, 140, 136, 141 | fmptco 7128 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) = (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) |
143 | 142 | oveq2d 7427 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) = (๐ ฮฃg (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))))) |
144 | | eqidd 2731 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) = (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) |
145 | | fveq2 6890 |
. . . . . . . 8
โข (๐ง = (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ (๐ธโ๐ง) = (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) |
146 | 31, 144, 136, 145 | fmptco 7128 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) = (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
147 | 146 | oveq2d 7427 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) = (๐ ฮฃg (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
148 | 143, 147 | oveq12d 7429 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = ((๐ ฮฃg
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
149 | | evlslem2.m |
. . . . . 6
โข ยท =
(.rโ๐) |
150 | | eqid 2730 |
. . . . . 6
โข
(0gโ๐) = (0gโ๐) |
151 | 134 | ad2antrr 722 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ธ:๐ตโถ(Baseโ๐)) |
152 | 151, 24 | ffvelcdmd 7086 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) โ
(Baseโ๐)) |
153 | 134 | ad2antrr 722 |
. . . . . . 7
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ ๐ธ:๐ตโถ(Baseโ๐)) |
154 | 153, 31 | ffvelcdmd 7086 |
. . . . . 6
โข (((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ ๐ท) โ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) โ
(Baseโ๐)) |
155 | 6 | mptex 7226 |
. . . . . . . . 9
โข (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โ
V |
156 | | funmpt 6585 |
. . . . . . . . 9
โข Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) |
157 | | fvex 6903 |
. . . . . . . . 9
โข
(0gโ๐) โ V |
158 | 155, 156,
157 | 3pm3.2i 1337 |
. . . . . . . 8
โข ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โง
(0gโ๐)
โ V) |
159 | 158 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โง
(0gโ๐)
โ V)) |
160 | | ssidd 4004 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))) |
161 | 3, 150 | ghmid 19136 |
. . . . . . . . . 10
โข (๐ธ โ (๐ GrpHom ๐) โ (๐ธโ(0gโ๐)) = (0gโ๐)) |
162 | 91, 161 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ธโ(0gโ๐)) = (0gโ๐)) |
163 | 6 | mptex 7226 |
. . . . . . . . . 10
โข (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ
V |
164 | 163 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ท) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )) โ
V) |
165 | 34 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (0gโ๐) โ V) |
166 | 160, 162,
164, 165 | suppssfv 8189 |
. . . . . . . 8
โข (๐ โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))) |
167 | 166 | adantr 479 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))) |
168 | | suppssfifsupp 9380 |
. . . . . . 7
โข ((((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) โง
(0gโ๐)
โ V) โง (((๐ โ
๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))
โ Fin โง ((๐ โ
๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) supp
(0gโ๐))))
โ (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) finSupp
(0gโ๐)) |
169 | 159, 108,
167, 168 | syl12anc 833 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))) finSupp
(0gโ๐)) |
170 | 6 | mptex 7226 |
. . . . . . . . 9
โข (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ
V |
171 | | funmpt 6585 |
. . . . . . . . 9
โข Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) |
172 | 170, 171,
157 | 3pm3.2i 1337 |
. . . . . . . 8
โข ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V) |
173 | 172 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V)) |
174 | | ssidd 4004 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))) |
175 | 6 | mptex 7226 |
. . . . . . . . . 10
โข (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ
V |
176 | 175 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ท) โ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )) โ
V) |
177 | 174, 162,
176, 165 | suppssfv 8189 |
. . . . . . . 8
โข (๐ โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))) |
178 | 177 | adantr 479 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))) |
179 | | suppssfifsupp 9380 |
. . . . . . 7
โข ((((๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โ V โง Fun
(๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) โง
(0gโ๐)
โ V) โง (((๐ โ
๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))
โ Fin โง ((๐ โ
๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) supp
(0gโ๐))
โ ((๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))) supp
(0gโ๐))))
โ (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) finSupp
(0gโ๐)) |
180 | 173, 109,
178, 179 | syl12anc 833 |
. . . . . 6
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))) finSupp
(0gโ๐)) |
181 | 132, 149,
150, 7, 7, 86, 152, 154, 169, 180 | gsumdixp 20207 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ โ ๐ท โฆ (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ ฮฃg
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
182 | 148, 181 | eqtrd 2770 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = (๐ ฮฃg
(๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))) ยท (๐ธโ(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
183 | 130, 139,
182 | 3eqtr4d 2780 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท, ๐ โ ๐ท โฆ ((๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))(.rโ๐)(๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = ((๐ ฮฃg
(๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
184 | 79, 115, 183 | 3eqtr2d 2776 |
. 2
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))))(.rโ๐)(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) = ((๐ ฮฃg
(๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
185 | 8 | adantr 479 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ผ โ ๐) |
186 | 11 | adantr 479 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐
โ Ring) |
187 | 12, 4, 16, 1, 185, 186, 20 | mplcoe4 21851 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฅ = (๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) |
188 | 12, 4, 16, 1, 185, 186, 27 | mplcoe4 21851 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฆ = (๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) |
189 | 187, 188 | oveq12d 7429 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(.rโ๐)๐ฆ) = ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))))(.rโ๐)(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
190 | 189 | fveq2d 6894 |
. 2
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ(๐ฅ(.rโ๐)๐ฆ)) = (๐ธโ((๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0
))))(.rโ๐)(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
191 | 187 | fveq2d 6894 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ๐ฅ) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))))) |
192 | 24 | fmpttd 7115 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))):๐ทโถ๐ต) |
193 | 1, 3, 82, 88, 7, 94, 192, 70 | gsummhm 19847 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))))) |
194 | 191, 193 | eqtr4d 2773 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ๐ฅ) = (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 )))))) |
195 | 188 | fveq2d 6894 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ๐ฆ) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
196 | 31 | fmpttd 7115 |
. . . . 5
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))):๐ทโถ๐ต) |
197 | 1, 3, 82, 88, 7, 94, 196, 77 | gsummhm 19847 |
. . . 4
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))) = (๐ธโ(๐ ฮฃg (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
198 | 195, 197 | eqtr4d 2773 |
. . 3
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ๐ฆ) = (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 )))))) |
199 | 194, 198 | oveq12d 7429 |
. 2
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ธโ๐ฅ) ยท (๐ธโ๐ฆ)) = ((๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฅโ๐), 0 ))))) ยท (๐ ฮฃg (๐ธ โ (๐ โ ๐ท โฆ (๐ โ ๐ท โฆ if(๐ = ๐, (๐ฆโ๐), 0 ))))))) |
200 | 184, 190,
199 | 3eqtr4d 2780 |
1
โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ธโ(๐ฅ(.rโ๐)๐ฆ)) = ((๐ธโ๐ฅ) ยท (๐ธโ๐ฆ))) |