Step | Hyp | Ref
| Expression |
1 | | hbtlem6.r |
. . 3
β’ (π β π
β LNoeR) |
2 | | lnrring 41468 |
. . . . 5
β’ (π
β LNoeR β π
β Ring) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π
β Ring) |
4 | | hbtlem6.i |
. . . 4
β’ (π β πΌ β π) |
5 | | hbtlem6.x |
. . . 4
β’ (π β π β
β0) |
6 | | hbtlem.p |
. . . . 5
β’ π = (Poly1βπ
) |
7 | | hbtlem.u |
. . . . 5
β’ π = (LIdealβπ) |
8 | | hbtlem.s |
. . . . 5
β’ π = (ldgIdlSeqβπ
) |
9 | | eqid 2737 |
. . . . 5
β’
(LIdealβπ
) =
(LIdealβπ
) |
10 | 6, 7, 8, 9 | hbtlem2 41480 |
. . . 4
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) β (LIdealβπ
)) |
11 | 3, 4, 5, 10 | syl3anc 1372 |
. . 3
β’ (π β ((πβπΌ)βπ) β (LIdealβπ
)) |
12 | | eqid 2737 |
. . . 4
β’
(RSpanβπ
) =
(RSpanβπ
) |
13 | 9, 12 | lnr2i 41472 |
. . 3
β’ ((π
β LNoeR β§ ((πβπΌ)βπ) β (LIdealβπ
)) β βπ β (π« ((πβπΌ)βπ) β© Fin)((πβπΌ)βπ) = ((RSpanβπ
)βπ)) |
14 | 1, 11, 13 | syl2anc 585 |
. 2
β’ (π β βπ β (π« ((πβπΌ)βπ) β© Fin)((πβπΌ)βπ) = ((RSpanβπ
)βπ)) |
15 | | elfpw 9305 |
. . . . 5
β’ (π β (π« ((πβπΌ)βπ) β© Fin) β (π β ((πβπΌ)βπ) β§ π β Fin)) |
16 | | fvex 6860 |
. . . . . . . . 9
β’
((coe1βπ)βπ) β V |
17 | | eqid 2737 |
. . . . . . . . 9
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) |
18 | 16, 17 | fnmpti 6649 |
. . . . . . . 8
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) Fn {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} |
19 | 18 | a1i 11 |
. . . . . . 7
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) Fn {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}) |
20 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β π β ((πβπΌ)βπ)) |
21 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
deg1 βπ
) =
( deg1 βπ
) |
22 | 6, 7, 8, 21 | hbtlem1 41479 |
. . . . . . . . . . 11
β’ ((π
β LNoeR β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
23 | 1, 4, 5, 22 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
24 | 17 | rnmpt 5915 |
. . . . . . . . . . 11
β’ ran
(π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = {π β£ βπ β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ)} |
25 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β (( deg1 βπ
)βπ) = (( deg1 βπ
)βπ)) |
26 | 25 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = π β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)βπ) β€ π)) |
27 | 26 | rexrab 3659 |
. . . . . . . . . . . 12
β’
(βπ β
{π β πΌ β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))) |
28 | 27 | abbii 2807 |
. . . . . . . . . . 11
β’ {π β£ βπ β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ)} = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} |
29 | 24, 28 | eqtri 2765 |
. . . . . . . . . 10
β’ ran
(π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} |
30 | 23, 29 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π β ((πβπΌ)βπ) = ran (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β ((πβπΌ)βπ) = ran (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
32 | 20, 31 | sseqtrd 3989 |
. . . . . . 7
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β π β ran (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
33 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β π β Fin) |
34 | | fipreima 9309 |
. . . . . . 7
β’ (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) Fn {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β ran (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β§ π β Fin) β βπ β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin)((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π) |
35 | 19, 32, 33, 34 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β βπ β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin)((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π) |
36 | | elfpw 9305 |
. . . . . . . . . 10
β’ (π β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin) β (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) |
37 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . 17
β’ {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β πΌ |
38 | | sstr2 3956 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β ({π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β πΌ β π β πΌ)) |
39 | 37, 38 | mpi 20 |
. . . . . . . . . . . . . . . 16
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β π β πΌ) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}) β π β πΌ) |
41 | | velpw 4570 |
. . . . . . . . . . . . . . 15
β’ (π β π« πΌ β π β πΌ) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}) β π β π« πΌ) |
43 | 42 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β π« πΌ) |
44 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β Fin) |
45 | 43, 44 | elind 4159 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β (π« πΌ β© Fin)) |
46 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π
β Ring) |
47 | 6 | ply1ring 21635 |
. . . . . . . . . . . . . . . . 17
β’ (π
β Ring β π β Ring) |
48 | 3, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β Ring) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β Ring) |
50 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π}) |
51 | 50, 37 | sstrdi 3961 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β πΌ) |
52 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ) =
(Baseβπ) |
53 | 52, 7 | lidlss 20696 |
. . . . . . . . . . . . . . . . . 18
β’ (πΌ β π β πΌ β (Baseβπ)) |
54 | 4, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β (Baseβπ)) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β πΌ β (Baseβπ)) |
56 | 51, 55 | sstrd 3959 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β (Baseβπ)) |
57 | | hbtlem6.n |
. . . . . . . . . . . . . . . 16
β’ π = (RSpanβπ) |
58 | 57, 52, 7 | rspcl 20708 |
. . . . . . . . . . . . . . 15
β’ ((π β Ring β§ π β (Baseβπ)) β (πβπ) β π) |
59 | 49, 56, 58 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β (πβπ) β π) |
60 | 5 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β
β0) |
61 | 6, 7, 8, 9 | hbtlem2 41480 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (πβπ) β π β§ π β β0) β ((πβ(πβπ))βπ) β (LIdealβπ
)) |
62 | 46, 59, 60, 61 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((πβ(πβπ))βπ) β (LIdealβπ
)) |
63 | | df-ima 5651 |
. . . . . . . . . . . . . . 15
β’ ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = ran ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) |
64 | 57, 52 | rspssid 20709 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Ring β§ π β (Baseβπ)) β π β (πβπ)) |
65 | 49, 56, 64 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β (πβπ)) |
66 | | ssrab 4035 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β (π β πΌ β§ βπ β π (( deg1 βπ
)βπ) β€ π)) |
67 | 66 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β βπ β π (( deg1 βπ
)βπ) β€ π) |
68 | 67 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β βπ β π (( deg1 βπ
)βπ) β€ π) |
69 | | ssrab 4035 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β (π β (πβπ) β§ βπ β π (( deg1 βπ
)βπ) β€ π)) |
70 | 65, 68, 69 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π}) |
71 | 70 | resmptd 5999 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) = (π β π β¦ ((coe1βπ)βπ))) |
72 | | resmpt 5996 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) = (π β π β¦ ((coe1βπ)βπ))) |
73 | 72 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) = (π β π β¦ ((coe1βπ)βπ))) |
74 | 71, 73 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) = ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π)) |
75 | | resss 5967 |
. . . . . . . . . . . . . . . . 17
β’ ((π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) β (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) |
76 | 74, 75 | eqsstrrdi 4004 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) β (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
77 | | rnss 5899 |
. . . . . . . . . . . . . . . 16
β’ (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) β (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β ran ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) β ran (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ran ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) βΎ π) β ran (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
79 | 63, 78 | eqsstrid 3997 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) β ran (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
80 | 6, 7, 8, 21 | hbtlem1 41479 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Ring β§ (πβπ) β π β§ π β β0) β ((πβ(πβπ))βπ) = {π β£ βπ β (πβπ)((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
81 | 46, 59, 60, 80 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((πβ(πβπ))βπ) = {π β£ βπ β (πβπ)((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
82 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) |
83 | 82 | rnmpt 5915 |
. . . . . . . . . . . . . . . 16
β’ ran
(π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = {π β£ βπ β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ)} |
84 | 26 | rexrab 3659 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
{π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ) β βπ β (πβπ)((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))) |
85 | 84 | abbii 2807 |
. . . . . . . . . . . . . . . 16
β’ {π β£ βπ β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π}π = ((coe1βπ)βπ)} = {π β£ βπ β (πβπ)((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} |
86 | 83, 85 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ ran
(π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) = {π β£ βπ β (πβπ)((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} |
87 | 81, 86 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((πβ(πβπ))βπ) = ran (π β {π β (πβπ) β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ))) |
88 | 79, 87 | sseqtrrd 3990 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) β ((πβ(πβπ))βπ)) |
89 | 12, 9 | rspssp 20712 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ ((πβ(πβπ))βπ) β (LIdealβπ
) β§ ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) β ((πβ(πβπ))βπ)) β ((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) β ((πβ(πβπ))βπ)) |
90 | 46, 62, 88, 89 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β ((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) β ((πβ(πβπ))βπ)) |
91 | 45, 90 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) β ((πβ(πβπ))βπ))) |
92 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β ((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) = ((RSpanβπ
)βπ)) |
93 | 92 | sseq1d 3980 |
. . . . . . . . . . . 12
β’ (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β (((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) β ((πβ(πβπ))βπ) β ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ))) |
94 | 93 | anbi2d 630 |
. . . . . . . . . . 11
β’ (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β ((π β (π« πΌ β© Fin) β§ ((RSpanβπ
)β((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π)) β ((πβ(πβπ))βπ)) β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)))) |
95 | 91, 94 | syl5ibcom 244 |
. . . . . . . . . 10
β’ ((π β§ (π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β§ π β Fin)) β (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)))) |
96 | 36, 95 | sylan2b 595 |
. . . . . . . . 9
β’ ((π β§ π β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin)) β (((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)))) |
97 | 96 | expimpd 455 |
. . . . . . . 8
β’ (π β ((π β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin) β§ ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π) β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)))) |
98 | 97 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β ((π β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin) β§ ((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π) β (π β (π« πΌ β© Fin) β§ ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)))) |
99 | 98 | reximdv2 3162 |
. . . . . 6
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β (βπ β (π« {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β© Fin)((π β {π β πΌ β£ (( deg1 βπ
)βπ) β€ π} β¦ ((coe1βπ)βπ)) β π) = π β βπ β (π« πΌ β© Fin)((RSpanβπ
)βπ) β ((πβ(πβπ))βπ))) |
100 | 35, 99 | mpd 15 |
. . . . 5
β’ ((π β§ (π β ((πβπΌ)βπ) β§ π β Fin)) β βπ β (π« πΌ β© Fin)((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)) |
101 | 15, 100 | sylan2b 595 |
. . . 4
β’ ((π β§ π β (π« ((πβπΌ)βπ) β© Fin)) β βπ β (π« πΌ β© Fin)((RSpanβπ
)βπ) β ((πβ(πβπ))βπ)) |
102 | | sseq1 3974 |
. . . . 5
β’ (((πβπΌ)βπ) = ((RSpanβπ
)βπ) β (((πβπΌ)βπ) β ((πβ(πβπ))βπ) β ((RSpanβπ
)βπ) β ((πβ(πβπ))βπ))) |
103 | 102 | rexbidv 3176 |
. . . 4
β’ (((πβπΌ)βπ) = ((RSpanβπ
)βπ) β (βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ) β βπ β (π« πΌ β© Fin)((RSpanβπ
)βπ) β ((πβ(πβπ))βπ))) |
104 | 101, 103 | syl5ibrcom 247 |
. . 3
β’ ((π β§ π β (π« ((πβπΌ)βπ) β© Fin)) β (((πβπΌ)βπ) = ((RSpanβπ
)βπ) β βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ))) |
105 | 104 | rexlimdva 3153 |
. 2
β’ (π β (βπ β (π« ((πβπΌ)βπ) β© Fin)((πβπΌ)βπ) = ((RSpanβπ
)βπ) β βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ))) |
106 | 14, 105 | mpd 15 |
1
β’ (π β βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ)) |