Step | Hyp | Ref
| Expression |
1 | | evl1gsumd.m |
. 2
β’ (π β βπ₯ β π π β π) |
2 | | evl1gsumd.n |
. . 3
β’ (π β π β Fin) |
3 | | raleq 3312 |
. . . . . . 7
β’ (π = β
β (βπ₯ β π π β π β βπ₯ β β
π β π)) |
4 | 3 | anbi2d 630 |
. . . . . 6
β’ (π = β
β ((π β§ βπ₯ β π π β π) β (π β§ βπ₯ β β
π β π))) |
5 | | mpteq1 5203 |
. . . . . . . . . 10
β’ (π = β
β (π₯ β π β¦ π) = (π₯ β β
β¦ π)) |
6 | 5 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = β
β (π Ξ£g
(π₯ β π β¦ π)) = (π Ξ£g (π₯ β β
β¦ π))) |
7 | 6 | fveq2d 6851 |
. . . . . . . 8
β’ (π = β
β (πβ(π Ξ£g (π₯ β π β¦ π))) = (πβ(π Ξ£g (π₯ β β
β¦ π)))) |
8 | 7 | fveq1d 6849 |
. . . . . . 7
β’ (π = β
β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ)) |
9 | | mpteq1 5203 |
. . . . . . . 8
β’ (π = β
β (π₯ β π β¦ ((πβπ)βπ)) = (π₯ β β
β¦ ((πβπ)βπ))) |
10 | 9 | oveq2d 7378 |
. . . . . . 7
β’ (π = β
β (π
Ξ£g
(π₯ β π β¦ ((πβπ)βπ))) = (π
Ξ£g (π₯ β β
β¦ ((πβπ)βπ)))) |
11 | 8, 10 | eqeq12d 2753 |
. . . . . 6
β’ (π = β
β (((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = (π
Ξ£g (π₯ β β
β¦ ((πβπ)βπ))))) |
12 | 4, 11 | imbi12d 345 |
. . . . 5
β’ (π = β
β (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β ((π β§ βπ₯ β β
π β π) β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = (π
Ξ£g (π₯ β β
β¦ ((πβπ)βπ)))))) |
13 | | raleq 3312 |
. . . . . . 7
β’ (π = π β (βπ₯ β π π β π β βπ₯ β π π β π)) |
14 | 13 | anbi2d 630 |
. . . . . 6
β’ (π = π β ((π β§ βπ₯ β π π β π) β (π β§ βπ₯ β π π β π))) |
15 | | mpteq1 5203 |
. . . . . . . . . 10
β’ (π = π β (π₯ β π β¦ π) = (π₯ β π β¦ π)) |
16 | 15 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β (π Ξ£g (π₯ β π β¦ π)) = (π Ξ£g (π₯ β π β¦ π))) |
17 | 16 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (πβ(π Ξ£g (π₯ β π β¦ π)))) |
18 | 17 | fveq1d 6849 |
. . . . . . 7
β’ (π = π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ)) |
19 | | mpteq1 5203 |
. . . . . . . 8
β’ (π = π β (π₯ β π β¦ ((πβπ)βπ)) = (π₯ β π β¦ ((πβπ)βπ))) |
20 | 19 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) |
21 | 18, 20 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))))) |
22 | 14, 21 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β ((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))))) |
23 | | raleq 3312 |
. . . . . . 7
β’ (π = (π βͺ {π}) β (βπ₯ β π π β π β βπ₯ β (π βͺ {π})π β π)) |
24 | 23 | anbi2d 630 |
. . . . . 6
β’ (π = (π βͺ {π}) β ((π β§ βπ₯ β π π β π) β (π β§ βπ₯ β (π βͺ {π})π β π))) |
25 | | mpteq1 5203 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β (π₯ β π β¦ π) = (π₯ β (π βͺ {π}) β¦ π)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β (π Ξ£g (π₯ β π β¦ π)) = (π Ξ£g (π₯ β (π βͺ {π}) β¦ π))) |
27 | 26 | fveq2d 6851 |
. . . . . . . 8
β’ (π = (π βͺ {π}) β (πβ(π Ξ£g (π₯ β π β¦ π))) = (πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))) |
28 | 27 | fveq1d 6849 |
. . . . . . 7
β’ (π = (π βͺ {π}) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ)) |
29 | | mpteq1 5203 |
. . . . . . . 8
β’ (π = (π βͺ {π}) β (π₯ β π β¦ ((πβπ)βπ)) = (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ))) |
30 | 29 | oveq2d 7378 |
. . . . . . 7
β’ (π = (π βͺ {π}) β (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))) |
31 | 28, 30 | eqeq12d 2753 |
. . . . . 6
β’ (π = (π βͺ {π}) β (((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ))))) |
32 | 24, 31 | imbi12d 345 |
. . . . 5
β’ (π = (π βͺ {π}) β (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β ((π β§ βπ₯ β (π βͺ {π})π β π) β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) |
33 | | raleq 3312 |
. . . . . . 7
β’ (π = π β (βπ₯ β π π β π β βπ₯ β π π β π)) |
34 | 33 | anbi2d 630 |
. . . . . 6
β’ (π = π β ((π β§ βπ₯ β π π β π) β (π β§ βπ₯ β π π β π))) |
35 | | mpteq1 5203 |
. . . . . . . . . 10
β’ (π = π β (π₯ β π β¦ π) = (π₯ β π β¦ π)) |
36 | 35 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β (π Ξ£g (π₯ β π β¦ π)) = (π Ξ£g (π₯ β π β¦ π))) |
37 | 36 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (πβ(π Ξ£g (π₯ β π β¦ π)))) |
38 | 37 | fveq1d 6849 |
. . . . . . 7
β’ (π = π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ)) |
39 | | mpteq1 5203 |
. . . . . . . 8
β’ (π = π β (π₯ β π β¦ ((πβπ)βπ)) = (π₯ β π β¦ ((πβπ)βπ))) |
40 | 39 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) |
41 | 38, 40 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))))) |
42 | 34, 41 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β ((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))))) |
43 | | mpt0 6648 |
. . . . . . . . . . . . 13
β’ (π₯ β β
β¦ π) = β
|
44 | 43 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (π Ξ£g
(π₯ β β
β¦
π)) = (π Ξ£g
β
) |
45 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(0gβπ) = (0gβπ) |
46 | 45 | gsum0 18546 |
. . . . . . . . . . . 12
β’ (π Ξ£g
β
) = (0gβπ) |
47 | 44, 46 | eqtri 2765 |
. . . . . . . . . . 11
β’ (π Ξ£g
(π₯ β β
β¦
π)) =
(0gβπ) |
48 | 47 | fveq2i 6850 |
. . . . . . . . . 10
β’ (πβ(π Ξ£g (π₯ β β
β¦ π))) = (πβ(0gβπ)) |
49 | | evl1gsumd.r |
. . . . . . . . . . . . . 14
β’ (π β π
β CRing) |
50 | | crngring 19983 |
. . . . . . . . . . . . . 14
β’ (π
β CRing β π
β Ring) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π
β Ring) |
52 | | evl1gsumd.p |
. . . . . . . . . . . . . 14
β’ π = (Poly1βπ
) |
53 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(algScβπ) =
(algScβπ) |
54 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(0gβπ
) = (0gβπ
) |
55 | 52, 53, 54, 45 | ply1scl0 21677 |
. . . . . . . . . . . . 13
β’ (π
β Ring β
((algScβπ)β(0gβπ
)) = (0gβπ)) |
56 | 51, 55 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((algScβπ)β(0gβπ
)) = (0gβπ)) |
57 | 56 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β (0gβπ) = ((algScβπ)β(0gβπ
))) |
58 | 57 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β (πβ(0gβπ)) = (πβ((algScβπ)β(0gβπ
)))) |
59 | 48, 58 | eqtrid 2789 |
. . . . . . . . 9
β’ (π β (πβ(π Ξ£g (π₯ β β
β¦ π))) = (πβ((algScβπ)β(0gβπ
)))) |
60 | 59 | fveq1d 6849 |
. . . . . . . 8
β’ (π β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = ((πβ((algScβπ)β(0gβπ
)))βπ)) |
61 | | evl1gsumd.q |
. . . . . . . . . 10
β’ π = (eval1βπ
) |
62 | | evl1gsumd.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ
) |
63 | | evl1gsumd.u |
. . . . . . . . . 10
β’ π = (Baseβπ) |
64 | | ringgrp 19976 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
β Grp) |
65 | 51, 64 | syl 17 |
. . . . . . . . . . 11
β’ (π β π
β Grp) |
66 | 62, 54 | grpidcl 18785 |
. . . . . . . . . . 11
β’ (π
β Grp β
(0gβπ
)
β π΅) |
67 | 65, 66 | syl 17 |
. . . . . . . . . 10
β’ (π β (0gβπ
) β π΅) |
68 | | evl1gsumd.y |
. . . . . . . . . 10
β’ (π β π β π΅) |
69 | 61, 52, 62, 53, 63, 49, 67, 68 | evl1scad 21717 |
. . . . . . . . 9
β’ (π β (((algScβπ)β(0gβπ
)) β π β§ ((πβ((algScβπ)β(0gβπ
)))βπ) = (0gβπ
))) |
70 | 69 | simprd 497 |
. . . . . . . 8
β’ (π β ((πβ((algScβπ)β(0gβπ
)))βπ) = (0gβπ
)) |
71 | 60, 70 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = (0gβπ
)) |
72 | | mpt0 6648 |
. . . . . . . . 9
β’ (π₯ β β
β¦ ((πβπ)βπ)) = β
|
73 | 72 | oveq2i 7373 |
. . . . . . . 8
β’ (π
Ξ£g
(π₯ β β
β¦
((πβπ)βπ))) = (π
Ξ£g
β
) |
74 | 54 | gsum0 18546 |
. . . . . . . 8
β’ (π
Ξ£g
β
) = (0gβπ
) |
75 | 73, 74 | eqtri 2765 |
. . . . . . 7
β’ (π
Ξ£g
(π₯ β β
β¦
((πβπ)βπ))) = (0gβπ
) |
76 | 71, 75 | eqtr4di 2795 |
. . . . . 6
β’ (π β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = (π
Ξ£g (π₯ β β
β¦ ((πβπ)βπ)))) |
77 | 76 | adantr 482 |
. . . . 5
β’ ((π β§ βπ₯ β β
π β π) β ((πβ(π Ξ£g (π₯ β β
β¦ π)))βπ) = (π
Ξ£g (π₯ β β
β¦ ((πβπ)βπ)))) |
78 | 61, 52, 62, 63, 49, 68 | evl1gsumdlem 21738 |
. . . . . . . 8
β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) |
79 | 78 | 3expia 1122 |
. . . . . . 7
β’ ((π β Fin β§ Β¬ π β π) β (π β ((βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ))))))) |
80 | 79 | a2d 29 |
. . . . . 6
β’ ((π β Fin β§ Β¬ π β π) β ((π β (βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))))) β (π β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ))))))) |
81 | | impexp 452 |
. . . . . 6
β’ (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β (π β (βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))))) |
82 | | impexp 452 |
. . . . . 6
β’ (((π β§ βπ₯ β (π βͺ {π})π β π) β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))) β (π β (βπ₯ β (π βͺ {π})π β π β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) |
83 | 80, 81, 82 | 3imtr4g 296 |
. . . . 5
β’ ((π β Fin β§ Β¬ π β π) β (((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) β ((π β§ βπ₯ β (π βͺ {π})π β π) β ((πβ(π Ξ£g (π₯ β (π βͺ {π}) β¦ π)))βπ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((πβπ)βπ)))))) |
84 | 12, 22, 32, 42, 77, 83 | findcard2s 9116 |
. . . 4
β’ (π β Fin β ((π β§ βπ₯ β π π β π) β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))))) |
85 | 84 | expd 417 |
. . 3
β’ (π β Fin β (π β (βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))))) |
86 | 2, 85 | mpcom 38 |
. 2
β’ (π β (βπ₯ β π π β π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ))))) |
87 | 1, 86 | mpd 15 |
1
β’ (π β ((πβ(π Ξ£g (π₯ β π β¦ π)))βπ) = (π
Ξ£g (π₯ β π β¦ ((πβπ)βπ)))) |