Step | Hyp | Ref
| Expression |
1 | | evlslem2.b |
. . . . 5
β’ π΅ = (Baseβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
3 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
4 | | evlslem2.d |
. . . . . . 7
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
5 | | ovex 7394 |
. . . . . . 7
β’
(β0 βm πΌ) β V |
6 | 4, 5 | rabex2 5295 |
. . . . . 6
β’ π· β V |
7 | 6 | a1i 11 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π· β V) |
8 | | evlslem2.i |
. . . . . . 7
β’ (π β πΌ β π) |
9 | | evlslem2.r |
. . . . . . . 8
β’ (π β π
β CRing) |
10 | | crngring 19984 |
. . . . . . . 8
β’ (π
β CRing β π
β Ring) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ (π β π
β Ring) |
12 | | evlslem2.p |
. . . . . . . 8
β’ π = (πΌ mPoly π
) |
13 | 12 | mplring 21447 |
. . . . . . 7
β’ ((πΌ β π β§ π
β Ring) β π β Ring) |
14 | 8, 11, 13 | syl2anc 585 |
. . . . . 6
β’ (π β π β Ring) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Ring) |
16 | | evlslem2.z |
. . . . . 6
β’ 0 =
(0gβπ
) |
17 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
18 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΌ β π) |
19 | 11 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π
β Ring) |
20 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β π΅) |
21 | 12, 17, 1, 4, 20 | mplelf 21427 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯:π·βΆ(Baseβπ
)) |
22 | 21 | ffvelcdmda 7039 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π₯βπ) β (Baseβπ
)) |
23 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π β π·) |
24 | 12, 4, 16, 17, 18, 19, 1, 22, 23 | mplmon2cl 21499 |
. . . . 5
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π β π· β¦ if(π = π, (π₯βπ), 0 )) β π΅) |
25 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΌ β π) |
26 | 11 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π
β Ring) |
27 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β π΅) |
28 | 12, 17, 1, 4, 27 | mplelf 21427 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦:π·βΆ(Baseβπ
)) |
29 | 28 | ffvelcdmda 7039 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π¦βπ) β (Baseβπ
)) |
30 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β π β π·) |
31 | 12, 4, 16, 17, 25, 26, 1, 29, 30 | mplmon2cl 21499 |
. . . . 5
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (π β π· β¦ if(π = π, (π¦βπ), 0 )) β π΅) |
32 | 6 | mptex 7177 |
. . . . . . . . . . . 12
β’ (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) β
V |
33 | | funmpt 6543 |
. . . . . . . . . . . 12
β’ Fun
(π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) |
34 | | fvex 6859 |
. . . . . . . . . . . 12
β’
(0gβπ) β V |
35 | 32, 33, 34 | 3pm3.2i 1340 |
. . . . . . . . . . 11
β’ ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) β V β§ Fun
(π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) β§
(0gβπ)
β V) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΅) β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) β V β§ Fun
(π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) β§
(0gβπ)
β V)) |
37 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΅) β π¦ β π΅) |
38 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΅) β π
β CRing) |
39 | 12, 1, 16, 37, 38 | mplelsfi 21424 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΅) β π¦ finSupp 0 ) |
40 | 39 | fsuppimpd 9319 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΅) β (π¦ supp 0 ) β
Fin) |
41 | 12, 17, 1, 4, 37 | mplelf 21427 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π΅) β π¦:π·βΆ(Baseβπ
)) |
42 | | ssidd 3971 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π΅) β (π¦ supp 0 ) β (π¦ supp 0 )) |
43 | 6 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π΅) β π· β V) |
44 | 16 | fvexi 6860 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β π΅) β 0 β V) |
46 | 41, 42, 43, 45 | suppssr 8131 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β (π¦βπ) = 0 ) |
47 | 46 | ifeq1d 4509 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β if(π = π, (π¦βπ), 0 ) = if(π = π, 0 , 0 )) |
48 | | ifid 4530 |
. . . . . . . . . . . . . 14
β’ if(π = π, 0 , 0 ) = 0 |
49 | 47, 48 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β if(π = π, (π¦βπ), 0 ) = 0 ) |
50 | 49 | mpteq2dv 5211 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β (π β π· β¦ if(π = π, (π¦βπ), 0 )) = (π β π· β¦ 0 )) |
51 | | ringgrp 19977 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β π
β Grp) |
52 | 11, 51 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π
β Grp) |
53 | 12, 4, 16, 3, 8, 52 | mpl0 21435 |
. . . . . . . . . . . . . 14
β’ (π β (0gβπ) = (π· Γ { 0 })) |
54 | | fconstmpt 5698 |
. . . . . . . . . . . . . 14
β’ (π· Γ { 0 }) = (π β π· β¦ 0 ) |
55 | 53, 54 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π β (0gβπ) = (π β π· β¦ 0 )) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β
(0gβπ) =
(π β π· β¦ 0 )) |
57 | 50, 56 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π΅) β§ π β (π· β (π¦ supp 0 ))) β (π β π· β¦ if(π = π, (π¦βπ), 0 )) =
(0gβπ)) |
58 | 57, 43 | suppss2 8135 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΅) β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))
β (π¦ supp 0
)) |
59 | | suppssfifsupp 9328 |
. . . . . . . . . 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 836 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΅) β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)) |
61 | 60 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ¦ β π΅ (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)) |
62 | | fveq1 6845 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (π¦βπ) = (π₯βπ)) |
63 | 62 | ifeq1d 4509 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β if(π = π, (π¦βπ), 0 ) = if(π = π, (π₯βπ), 0 )) |
64 | 63 | mpteq2dv 5211 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π β π· β¦ if(π = π, (π¦βπ), 0 )) = (π β π· β¦ if(π = π, (π₯βπ), 0 ))) |
65 | 64 | mpteq2dv 5211 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) = (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))) |
66 | 65 | breq1d 5119 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)
β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) finSupp
(0gβπ))) |
67 | 66 | cbvralvw 3224 |
. . . . . . . 8
β’
(βπ¦ β
π΅ (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)
β βπ₯ β
π΅ (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) finSupp
(0gβπ)) |
68 | 61, 67 | sylib 217 |
. . . . . . 7
β’ (π β βπ₯ β π΅ (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) finSupp
(0gβπ)) |
69 | 68 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) finSupp
(0gβπ)) |
70 | 69 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) finSupp
(0gβπ)) |
71 | | equequ2 2030 |
. . . . . . . . 9
β’ (π = π β (π = π β π = π)) |
72 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (π¦βπ) = (π¦βπ)) |
73 | 71, 72 | ifbieq1d 4514 |
. . . . . . . 8
β’ (π = π β if(π = π, (π¦βπ), 0 ) = if(π = π, (π¦βπ), 0 )) |
74 | 73 | mpteq2dv 5211 |
. . . . . . 7
β’ (π = π β (π β π· β¦ if(π = π, (π¦βπ), 0 )) = (π β π· β¦ if(π = π, (π¦βπ), 0 ))) |
75 | 74 | cbvmptv 5222 |
. . . . . 6
β’ (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) = (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) |
76 | 60 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)) |
77 | 75, 76 | eqbrtrid 5144 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) finSupp
(0gβπ)) |
78 | 1, 2, 3, 7, 7, 15,
24, 31, 70, 77 | gsumdixp 20041 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0
))))(.rβπ)(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))) = (π Ξ£g (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
79 | 78 | fveq2d 6850 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ((π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0
))))(.rβπ)(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (πΈβ(π Ξ£g (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
80 | | ringcmn 20011 |
. . . . . 6
β’ (π β Ring β π β CMnd) |
81 | 14, 80 | syl 17 |
. . . . 5
β’ (π β π β CMnd) |
82 | 81 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β CMnd) |
83 | | evlslem2.s |
. . . . . . 7
β’ (π β π β CRing) |
84 | | crngring 19984 |
. . . . . . 7
β’ (π β CRing β π β Ring) |
85 | 83, 84 | syl 17 |
. . . . . 6
β’ (π β π β Ring) |
86 | 85 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Ring) |
87 | | ringmnd 19982 |
. . . . 5
β’ (π β Ring β π β Mnd) |
88 | 86, 87 | syl 17 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Mnd) |
89 | 6, 6 | xpex 7691 |
. . . . 5
β’ (π· Γ π·) β V |
90 | 89 | a1i 11 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π· Γ π·) β V) |
91 | | evlslem2.e1 |
. . . . . 6
β’ (π β πΈ β (π GrpHom π)) |
92 | | ghmmhm 19026 |
. . . . . 6
β’ (πΈ β (π GrpHom π) β πΈ β (π MndHom π)) |
93 | 91, 92 | syl 17 |
. . . . 5
β’ (π β πΈ β (π MndHom π)) |
94 | 93 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΈ β (π MndHom π)) |
95 | 14 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β π β Ring) |
96 | 24 | adantrr 716 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (π β π· β¦ if(π = π, (π₯βπ), 0 )) β π΅) |
97 | 31 | adantrl 715 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (π β π· β¦ if(π = π, (π¦βπ), 0 )) β π΅) |
98 | 1, 2 | ringcl 19989 |
. . . . . . 7
β’ ((π β Ring β§ (π β π· β¦ if(π = π, (π₯βπ), 0 )) β π΅ β§ (π β π· β¦ if(π = π, (π¦βπ), 0 )) β π΅) β ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))) β π΅) |
99 | 95, 96, 97, 98 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))) β π΅) |
100 | 99 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β βπ β π· βπ β π· ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))) β π΅) |
101 | | eqid 2733 |
. . . . . 6
β’ (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) = (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) |
102 | 101 | fmpo 8004 |
. . . . 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 8016 |
. . . . . . 7
β’ (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β
V |
105 | 101 | mpofun 7484 |
. . . . . . 7
β’ Fun
(π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) |
106 | 104, 105,
34 | 3pm3.2i 1340 |
. . . . . 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 9319 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))
β Fin) |
109 | 77 | fsuppimpd 9319 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))
β Fin) |
110 | | xpfi 9267 |
. . . . . 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 585 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))
Γ ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ)))
β Fin) |
112 | 1, 3, 2, 15, 24, 31, 7, 7 | evlslem4 21507 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) supp
(0gβπ))
β (((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))
Γ ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ)))) |
113 | | suppssfifsupp 9328 |
. . . . 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 836 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) finSupp
(0gβπ)) |
115 | 1, 3, 82, 88, 90, 94, 103, 114 | gsummhm 19723 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (πΈβ(π Ξ£g (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
116 | 8 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β πΌ β π) |
117 | 9 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β π
β CRing) |
118 | | eqid 2733 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
119 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β π β π·) |
120 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β π β π·) |
121 | 22 | adantrr 716 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (π₯βπ) β (Baseβπ
)) |
122 | 29 | adantrl 715 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (π¦βπ) β (Baseβπ
)) |
123 | 12, 4, 16, 17, 116, 117, 2, 118, 119, 120, 121, 122 | mplmon2mul 21500 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))) = (π β π· β¦ if(π = (π βf + π), ((π₯βπ)(.rβπ
)(π¦βπ)), 0 ))) |
124 | 123 | fveq2d 6850 |
. . . . . . . 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 469 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (πΈβ(π β π· β¦ if(π = (π βf + π), ((π₯βπ)(.rβπ
)(π¦βπ)), 0 ))) = ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
127 | 124, 126 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ (π β π· β§ π β π·)) β (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) = ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
128 | 127 | 3impb 1116 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π· β§ π β π·) β (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) = ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
129 | 128 | mpoeq3dva 7438 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π·, π β π· β¦ (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) = (π β π·, π β π· β¦ ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
130 | 129 | oveq2d 7377 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (π β π·, π β π· β¦ (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (π Ξ£g
(π β π·, π β π· β¦ ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
131 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))) = (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
132 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
133 | 1, 132 | ghmf 19020 |
. . . . . . . . 9
β’ (πΈ β (π GrpHom π) β πΈ:π΅βΆ(Baseβπ)) |
134 | 91, 133 | syl 17 |
. . . . . . . 8
β’ (π β πΈ:π΅βΆ(Baseβπ)) |
135 | 134 | feqmptd 6914 |
. . . . . . 7
β’ (π β πΈ = (π§ β π΅ β¦ (πΈβπ§))) |
136 | 135 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΈ = (π§ β π΅ β¦ (πΈβπ§))) |
137 | | fveq2 6846 |
. . . . . 6
β’ (π§ = ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))) β (πΈβπ§) = (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
138 | 99, 131, 136, 137 | fmpoco 8031 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈ β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) = (π β π·, π β π· β¦ (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
139 | 138 | oveq2d 7377 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (π Ξ£g
(π β π·, π β π· β¦ (πΈβ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
140 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) = (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))) |
141 | | fveq2 6846 |
. . . . . . . 8
β’ (π§ = (π β π· β¦ if(π = π, (π₯βπ), 0 )) β (πΈβπ§) = (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) |
142 | 24, 140, 136, 141 | fmptco 7079 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))) = (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))))) |
143 | 142 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) = (π Ξ£g (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))))) |
144 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) = (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))) |
145 | | fveq2 6846 |
. . . . . . . 8
β’ (π§ = (π β π· β¦ if(π = π, (π¦βπ), 0 )) β (πΈβπ§) = (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) |
146 | 31, 144, 136, 145 | fmptco 7079 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))) = (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
147 | 146 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))) = (π Ξ£g (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
148 | 143, 147 | oveq12d 7379 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = ((π Ξ£g
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
149 | | evlslem2.m |
. . . . . 6
β’ Β· =
(.rβπ) |
150 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
151 | 134 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΈ:π΅βΆ(Baseβπ)) |
152 | 151, 24 | ffvelcdmd 7040 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) β
(Baseβπ)) |
153 | 134 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β πΈ:π΅βΆ(Baseβπ)) |
154 | 153, 31 | ffvelcdmd 7040 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π·) β (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))) β
(Baseβπ)) |
155 | 6 | mptex 7177 |
. . . . . . . . 9
β’ (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) β
V |
156 | | funmpt 6543 |
. . . . . . . . 9
β’ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) |
157 | | fvex 6859 |
. . . . . . . . 9
β’
(0gβπ) β V |
158 | 155, 156,
157 | 3pm3.2i 1340 |
. . . . . . . 8
β’ ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) β V β§ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) β§
(0gβπ)
β V) |
159 | 158 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) β V β§ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) β§
(0gβπ)
β V)) |
160 | | ssidd 3971 |
. . . . . . . . 9
β’ (π β ((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))) |
161 | 3, 150 | ghmid 19022 |
. . . . . . . . . 10
β’ (πΈ β (π GrpHom π) β (πΈβ(0gβπ)) = (0gβπ)) |
162 | 91, 161 | syl 17 |
. . . . . . . . 9
β’ (π β (πΈβ(0gβπ)) = (0gβπ)) |
163 | 6 | mptex 7177 |
. . . . . . . . . 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 8137 |
. . . . . . . 8
β’ (π β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))) |
167 | 166 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))) supp
(0gβπ))) |
168 | | suppssfifsupp 9328 |
. . . . . . 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 836 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 )))) finSupp
(0gβπ)) |
170 | 6 | mptex 7177 |
. . . . . . . . 9
β’ (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β
V |
171 | | funmpt 6543 |
. . . . . . . . 9
β’ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) |
172 | 170, 171,
157 | 3pm3.2i 1340 |
. . . . . . . 8
β’ ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β V β§ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β§
(0gβπ)
β V) |
173 | 172 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β V β§ Fun
(π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) β§
(0gβπ)
β V)) |
174 | | ssidd 3971 |
. . . . . . . . 9
β’ (π β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))) |
175 | 6 | mptex 7177 |
. . . . . . . . . 10
β’ (π β π· β¦ if(π = π, (π¦βπ), 0 )) β
V |
176 | 175 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (π β π· β¦ if(π = π, (π¦βπ), 0 )) β
V) |
177 | 174, 162,
176, 165 | suppssfv 8137 |
. . . . . . . 8
β’ (π β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))) |
178 | 177 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) supp
(0gβπ))
β ((π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))) supp
(0gβπ))) |
179 | | suppssfifsupp 9328 |
. . . . . . 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 836 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))) finSupp
(0gβπ)) |
181 | 132, 149,
150, 7, 7, 86, 152, 154, 169, 180 | gsumdixp 20041 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π Ξ£g (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (π β π· β¦ (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (π Ξ£g
(π β π·, π β π· β¦ ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
182 | 148, 181 | eqtrd 2773 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = (π Ξ£g
(π β π·, π β π· β¦ ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
183 | 130, 139,
182 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π·, π β π· β¦ ((π β π· β¦ if(π = π, (π₯βπ), 0
))(.rβπ)(π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = ((π Ξ£g
(πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
184 | 79, 115, 183 | 3eqtr2d 2779 |
. 2
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ((π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0
))))(.rβπ)(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) = ((π Ξ£g
(πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
185 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΌ β π) |
186 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π
β Ring) |
187 | 12, 4, 16, 1, 185, 186, 20 | mplcoe4 21502 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ = (π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) |
188 | 12, 4, 16, 1, 185, 186, 27 | mplcoe4 21502 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ = (π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))) |
189 | 187, 188 | oveq12d 7379 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπ)π¦) = ((π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0
))))(.rβπ)(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
190 | 189 | fveq2d 6850 |
. 2
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(.rβπ)π¦)) = (πΈβ((π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0
))))(.rβπ)(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
191 | 187 | fveq2d 6850 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ₯) = (πΈβ(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))))) |
192 | 24 | fmpttd 7067 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))):π·βΆπ΅) |
193 | 1, 3, 82, 88, 7, 94, 192, 70 | gsummhm 19723 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) = (πΈβ(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))))) |
194 | 191, 193 | eqtr4d 2776 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ₯) = (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 )))))) |
195 | 188 | fveq2d 6850 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ¦) = (πΈβ(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
196 | 31 | fmpttd 7067 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))):π·βΆπ΅) |
197 | 1, 3, 82, 88, 7, 94, 196, 77 | gsummhm 19723 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))) = (πΈβ(π Ξ£g (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
198 | 195, 197 | eqtr4d 2776 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβπ¦) = (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 )))))) |
199 | 194, 198 | oveq12d 7379 |
. 2
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πΈβπ₯) Β· (πΈβπ¦)) = ((π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π₯βπ), 0 ))))) Β· (π Ξ£g (πΈ β (π β π· β¦ (π β π· β¦ if(π = π, (π¦βπ), 0 ))))))) |
200 | 184, 190,
199 | 3eqtr4d 2783 |
1
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(.rβπ)π¦)) = ((πΈβπ₯) Β· (πΈβπ¦))) |