Step | Hyp | Ref
| Expression |
1 | | ralunb 4152 |
. . 3
β’
(βπ₯ β
(π βͺ {π})π β π΅ β (βπ₯ β π π β π΅ β§ βπ₯ β {π}π β π΅)) |
2 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π¦π |
3 | | nfcsb1v 3881 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯β¦π¦ / π₯β¦π |
4 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β π = β¦π¦ / π₯β¦π) |
5 | 2, 3, 4 | cbvmpt 5217 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π βͺ {π}) β¦ π) = (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦π) |
6 | 5 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
β’ (π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)) = (π Ξ£g (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦π)) |
7 | | coe1fzgsumd.b |
. . . . . . . . . . . . . . . 16
β’ π΅ = (Baseβπ) |
8 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(+gβπ) = (+gβπ) |
9 | | coe1fzgsumd.r |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π
β Ring) |
10 | | coe1fzgsumd.p |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (Poly1βπ
) |
11 | 10 | ply1ring 21635 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β Ring β π β Ring) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β Ring) |
13 | | ringcmn 20008 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Ring β π β CMnd) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β CMnd) |
15 | 14 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ Β¬ π β π β§ π) β π β CMnd) |
16 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β π β CMnd) |
17 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β π β Fin) |
18 | | rspcsbela 4396 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β π β§ βπ₯ β π π β π΅) β β¦π¦ / π₯β¦π β π΅) |
19 | 18 | expcom 415 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯ β
π π β π΅ β (π¦ β π β β¦π¦ / π₯β¦π β π΅)) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β (π¦ β π β β¦π¦ / π₯β¦π β π΅)) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π¦ β π β β¦π¦ / π₯β¦π β π΅)) |
22 | 21 | imp 408 |
. . . . . . . . . . . . . . . 16
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ π¦ β π) β β¦π¦ / π₯β¦π β π΅) |
23 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β π β V) |
25 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β Β¬ π β π) |
26 | | vsnid 4624 |
. . . . . . . . . . . . . . . . . 18
β’ π β {π} |
27 | | rspcsbela 4396 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β {π} β§ βπ₯ β {π}π β π΅) β β¦π / π₯β¦π β π΅) |
28 | 26, 27 | mpan 689 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯ β
{π}π β π΅ β β¦π / π₯β¦π β π΅) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β β¦π / π₯β¦π β π΅) |
30 | | csbeq1 3859 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β β¦π¦ / π₯β¦π = β¦π / π₯β¦π) |
31 | 7, 8, 16, 17, 22, 24, 25, 29, 30 | gsumunsn 19742 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π Ξ£g (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦π)) = ((π Ξ£g (π¦ β π β¦ β¦π¦ / π₯β¦π))(+gβπ)β¦π / π₯β¦π)) |
32 | 6, 31 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π Ξ£g (π₯ β (π βͺ {π}) β¦ π)) = ((π Ξ£g (π¦ β π β¦ β¦π¦ / π₯β¦π))(+gβπ)β¦π / π₯β¦π)) |
33 | 2, 3, 4 | cbvmpt 5217 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ π) = (π¦ β π β¦ β¦π¦ / π₯β¦π) |
34 | 33 | eqcomi 2742 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β¦ β¦π¦ / π₯β¦π) = (π₯ β π β¦ π) |
35 | 34 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
β’ (π Ξ£g
(π¦ β π β¦ β¦π¦ / π₯β¦π)) = (π Ξ£g (π₯ β π β¦ π)) |
36 | 35 | oveq1i 7368 |
. . . . . . . . . . . . . 14
β’ ((π Ξ£g
(π¦ β π β¦ β¦π¦ / π₯β¦π))(+gβπ)β¦π / π₯β¦π) = ((π Ξ£g (π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π) |
37 | 32, 36 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π Ξ£g (π₯ β (π βͺ {π}) β¦ π)) = ((π Ξ£g (π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π)) |
38 | 37 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π))) = (coe1β((π Ξ£g
(π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π))) |
39 | 38 | fveq1d 6845 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = ((coe1β((π Ξ£g
(π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π))βπΎ)) |
40 | 9 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ Β¬ π β π β§ π) β π
β Ring) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β π
β Ring) |
42 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β βπ₯ β π π β π΅) |
43 | 7, 16, 17, 42 | gsummptcl 19749 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π Ξ£g (π₯ β π β¦ π)) β π΅) |
44 | | coe1fzgsumd.k |
. . . . . . . . . . . . . 14
β’ (π β πΎ β
β0) |
45 | 44 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ Β¬ π β π β§ π) β πΎ β
β0) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β πΎ β
β0) |
47 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβπ
) = (+gβπ
) |
48 | 10, 7, 8, 47 | coe1addfv 21652 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ (π Ξ£g
(π₯ β π β¦ π)) β π΅ β§ β¦π / π₯β¦π β π΅) β§ πΎ β β0) β
((coe1β((π
Ξ£g (π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π))βπΎ) = (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ)(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
49 | 41, 43, 29, 46, 48 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β ((coe1β((π Ξ£g
(π₯ β π β¦ π))(+gβπ)β¦π / π₯β¦π))βπΎ) = (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ)(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
50 | 39, 49 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ)(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
51 | | oveq1 7365 |
. . . . . . . . . 10
β’
(((coe1β(π Ξ£g (π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))) β (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ)(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ)) = ((π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
52 | 50, 51 | sylan9eq 2793 |
. . . . . . . . 9
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = ((π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
53 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π¦((coe1βπ)βπΎ) |
54 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
β’
β²π₯β¦π¦ / π₯β¦((coe1βπ)βπΎ) |
55 | | csbeq1a 3870 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((coe1βπ)βπΎ) = β¦π¦ / π₯β¦((coe1βπ)βπΎ)) |
56 | 53, 54, 55 | cbvmpt 5217 |
. . . . . . . . . . . . 13
β’ (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)) = (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)) |
57 | 56 | oveq2i 7369 |
. . . . . . . . . . . 12
β’ (π
Ξ£g
(π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))) = (π
Ξ£g (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ))) |
58 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ
) =
(Baseβπ
) |
59 | | ringcmn 20008 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β π
β CMnd) |
60 | 9, 59 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π
β CMnd) |
61 | 60 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ Β¬ π β π β§ π) β π
β CMnd) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β π
β CMnd) |
63 | | csbfv12 6891 |
. . . . . . . . . . . . . . 15
β’
β¦π¦ /
π₯β¦((coe1βπ)βπΎ) = (β¦π¦ / π₯β¦(coe1βπ)ββ¦π¦ / π₯β¦πΎ) |
64 | | csbfv2g 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β V β
β¦π¦ / π₯β¦(coe1βπ) =
(coe1ββ¦π¦ / π₯β¦π)) |
65 | 64 | elv 3450 |
. . . . . . . . . . . . . . . 16
β’
β¦π¦ /
π₯β¦(coe1βπ) =
(coe1ββ¦π¦ / π₯β¦π) |
66 | | csbconstg 3875 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β V β
β¦π¦ / π₯β¦πΎ = πΎ) |
67 | 66 | elv 3450 |
. . . . . . . . . . . . . . . 16
β’
β¦π¦ /
π₯β¦πΎ = πΎ |
68 | 65, 67 | fveq12i 6849 |
. . . . . . . . . . . . . . 15
β’
(β¦π¦ /
π₯β¦(coe1βπ)ββ¦π¦ / π₯β¦πΎ) =
((coe1ββ¦π¦ / π₯β¦π)βπΎ) |
69 | 63, 68 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’
β¦π¦ /
π₯β¦((coe1βπ)βπΎ) =
((coe1ββ¦π¦ / π₯β¦π)βπΎ) |
70 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(coe1ββ¦π¦ / π₯β¦π) =
(coe1ββ¦π¦ / π₯β¦π) |
71 | 70, 7, 10, 58 | coe1f 21598 |
. . . . . . . . . . . . . . . 16
β’
(β¦π¦ /
π₯β¦π β π΅ β
(coe1ββ¦π¦ / π₯β¦π):β0βΆ(Baseβπ
)) |
72 | 22, 71 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ π¦ β π) β
(coe1ββ¦π¦ / π₯β¦π):β0βΆ(Baseβπ
)) |
73 | 45 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β πΎ β
β0) |
74 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ π¦ β π) β πΎ β
β0) |
75 | 72, 74 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ π¦ β π) β
((coe1ββ¦π¦ / π₯β¦π)βπΎ) β (Baseβπ
)) |
76 | 69, 75 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ π¦ β π) β β¦π¦ / π₯β¦((coe1βπ)βπΎ) β (Baseβπ
)) |
77 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(coe1ββ¦π / π₯β¦π) =
(coe1ββ¦π / π₯β¦π) |
78 | 77, 7, 10, 58 | coe1f 21598 |
. . . . . . . . . . . . . . 15
β’
(β¦π /
π₯β¦π β π΅ β
(coe1ββ¦π / π₯β¦π):β0βΆ(Baseβπ
)) |
79 | 29, 78 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β
(coe1ββ¦π / π₯β¦π):β0βΆ(Baseβπ
)) |
80 | 79, 46 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β
((coe1ββ¦π / π₯β¦π)βπΎ) β (Baseβπ
)) |
81 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
82 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
β’
β²π₯coe1 |
83 | | nfcsb1v 3881 |
. . . . . . . . . . . . . . . 16
β’
β²π₯β¦π / π₯β¦π |
84 | 82, 83 | nffv 6853 |
. . . . . . . . . . . . . . 15
β’
β²π₯(coe1ββ¦π / π₯β¦π) |
85 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π₯πΎ |
86 | 84, 85 | nffv 6853 |
. . . . . . . . . . . . . 14
β’
β²π₯((coe1ββ¦π / π₯β¦π)βπΎ) |
87 | | csbeq1a 3870 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β π = β¦π / π₯β¦π) |
88 | 87 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (coe1βπ) =
(coe1ββ¦π / π₯β¦π)) |
89 | 88 | fveq1d 6845 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((coe1βπ)βπΎ) =
((coe1ββ¦π / π₯β¦π)βπΎ)) |
90 | 81, 86, 89 | csbhypf 3885 |
. . . . . . . . . . . . 13
β’ (π¦ = π β β¦π¦ / π₯β¦((coe1βπ)βπΎ) =
((coe1ββ¦π / π₯β¦π)βπΎ)) |
91 | 58, 47, 62, 17, 76, 24, 25, 80, 90 | gsumunsn 19742 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π
Ξ£g (π¦ β (π βͺ {π}) β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ))) = ((π
Ξ£g (π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
92 | 57, 91 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))) = ((π
Ξ£g (π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ))) |
93 | 53, 54, 55 | cbvmpt 5217 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β¦ ((coe1βπ)βπΎ)) = (π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)) |
94 | 93 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)) = (π₯ β π β¦ ((coe1βπ)βπΎ)) |
95 | 94 | oveq2i 7369 |
. . . . . . . . . . . 12
β’ (π
Ξ£g
(π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ))) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))) |
96 | 95 | oveq1i 7368 |
. . . . . . . . . . 11
β’ ((π
Ξ£g
(π¦ β π β¦ β¦π¦ / π₯β¦((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ)) = ((π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ)) |
97 | 92, 96 | eqtr2di 2790 |
. . . . . . . . . 10
β’ ((((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β ((π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ)) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))) |
98 | 97 | adantr 482 |
. . . . . . . . 9
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β ((π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))(+gβπ
)((coe1ββ¦π / π₯β¦π)βπΎ)) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))) |
99 | 52, 98 | eqtrd 2773 |
. . . . . . . 8
β’
(((((π β Fin
β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β§ βπ₯ β {π}π β π΅) β§ ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))) |
100 | 99 | exp31 421 |
. . . . . . 7
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β (βπ₯ β {π}π β π΅ β (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) |
101 | 100 | com23 86 |
. . . . . 6
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ βπ₯ β π π β π΅) β (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))) β (βπ₯ β {π}π β π΅ β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) |
102 | 101 | ex 414 |
. . . . 5
β’ ((π β Fin β§ Β¬ π β π β§ π) β (βπ₯ β π π β π΅ β (((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))) β (βπ₯ β {π}π β π΅ β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))))))) |
103 | 102 | a2d 29 |
. . . 4
β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π΅ β ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β (βπ₯ β π π β π΅ β (βπ₯ β {π}π β π΅ β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))))))) |
104 | 103 | imp4b 423 |
. . 3
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ (βπ₯ β π π β π΅ β ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))))) β ((βπ₯ β π π β π΅ β§ βπ₯ β {π}π β π΅) β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))))) |
105 | 1, 104 | biimtrid 241 |
. 2
β’ (((π β Fin β§ Β¬ π β π β§ π) β§ (βπ₯ β π π β π΅ β ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ))))) β (βπ₯ β (π βͺ {π})π β π΅ β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ))))) |
106 | 105 | ex 414 |
1
β’ ((π β Fin β§ Β¬ π β π β§ π) β ((βπ₯ β π π β π΅ β ((coe1β(π Ξ£g
(π₯ β π β¦ π)))βπΎ) = (π
Ξ£g (π₯ β π β¦ ((coe1βπ)βπΎ)))) β (βπ₯ β (π βͺ {π})π β π΅ β ((coe1β(π Ξ£g
(π₯ β (π βͺ {π}) β¦ π)))βπΎ) = (π
Ξ£g (π₯ β (π βͺ {π}) β¦ ((coe1βπ)βπΎ)))))) |