Step | Hyp | Ref
| Expression |
1 | | elqaa.1 |
. 2
β’ (π β π΄ β β) |
2 | | cnex 11139 |
. . . . . . . 8
β’ β
β V |
3 | 2 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
4 | | elqaa.6 |
. . . . . . . . 9
β’ π
= (seq0( Β· , π)β(degβπΉ)) |
5 | 4 | fvexi 6861 |
. . . . . . . 8
β’ π
β V |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ π§ β β) β π
β V) |
7 | | fvexd 6862 |
. . . . . . 7
β’ ((π β§ π§ β β) β (πΉβπ§) β V) |
8 | | fconstmpt 5699 |
. . . . . . . 8
β’ (β
Γ {π
}) = (π§ β β β¦ π
) |
9 | 8 | a1i 11 |
. . . . . . 7
β’ (π β (β Γ {π
}) = (π§ β β β¦ π
)) |
10 | | elqaa.2 |
. . . . . . . . . 10
β’ (π β πΉ β ((Polyββ) β
{0π})) |
11 | 10 | eldifad 3927 |
. . . . . . . . 9
β’ (π β πΉ β
(Polyββ)) |
12 | | plyf 25575 |
. . . . . . . . 9
β’ (πΉ β (Polyββ)
β πΉ:ββΆβ) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
14 | 13 | feqmptd 6915 |
. . . . . . 7
β’ (π β πΉ = (π§ β β β¦ (πΉβπ§))) |
15 | 3, 6, 7, 9, 14 | offval2 7642 |
. . . . . 6
β’ (π β ((β Γ {π
}) βf Β·
πΉ) = (π§ β β β¦ (π
Β· (πΉβπ§)))) |
16 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β (0...(degβπΉ)) β Fin) |
17 | | nn0uz 12812 |
. . . . . . . . . . . . . 14
β’
β0 = (β€β₯β0) |
18 | | 0zd 12518 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β€) |
19 | | ssrab2 4042 |
. . . . . . . . . . . . . . 15
β’ {π β β β£ ((π΅βπ) Β· π) β β€} β
β |
20 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π΅βπ) = (π΅βπ)) |
21 | 20 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π΅βπ) Β· π) = ((π΅βπ) Β· π)) |
22 | 21 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((π΅βπ) Β· π) β β€ β ((π΅βπ) Β· π) β β€)) |
23 | 22 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β {π β β β£ ((π΅βπ) Β· π) β β€} = {π β β β£ ((π΅βπ) Β· π) β β€}) |
24 | 23 | infeq1d 9420 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < ) =
inf({π β β
β£ ((π΅βπ) Β· π) β β€}, β, <
)) |
25 | | elqaa.5 |
. . . . . . . . . . . . . . . . . 18
β’ π = (π β β0 β¦
inf({π β β
β£ ((π΅βπ) Β· π) β β€}, β, <
)) |
26 | | ltso 11242 |
. . . . . . . . . . . . . . . . . . 19
β’ < Or
β |
27 | 26 | infex 9436 |
. . . . . . . . . . . . . . . . . 18
β’
inf({π β
β β£ ((π΅βπ) Β· π) β β€}, β, < ) β
V |
28 | 24, 25, 27 | fvmpt 6953 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (πβπ) = inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, <
)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (πβπ) = inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, <
)) |
30 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . 18
β’ β =
(β€β₯β1) |
31 | 19, 30 | sseqtri 3985 |
. . . . . . . . . . . . . . . . 17
β’ {π β β β£ ((π΅βπ) Β· π) β β€} β
(β€β₯β1) |
32 | | 0z 12517 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β€ |
33 | | zq 12886 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 β
β€ β 0 β β) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
β |
35 | | elqaa.4 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π΅ = (coeffβπΉ) |
36 | 35 | coef2 25608 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ β (Polyββ)
β§ 0 β β) β π΅:β0βΆβ) |
37 | 11, 34, 36 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅:β0βΆβ) |
38 | 37 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β0) β (π΅βπ) β β) |
39 | | qmulz 12883 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅βπ) β β β βπ β β ((π΅βπ) Β· π) β β€) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β
βπ β β
((π΅βπ) Β· π) β β€) |
41 | | rabn0 4350 |
. . . . . . . . . . . . . . . . . 18
β’ ({π β β β£ ((π΅βπ) Β· π) β β€} β β
β
βπ β β
((π΅βπ) Β· π) β β€) |
42 | 40, 41 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β {π β β β£ ((π΅βπ) Β· π) β β€} β
β
) |
43 | | infssuzcl 12864 |
. . . . . . . . . . . . . . . . 17
β’ (({π β β β£ ((π΅βπ) Β· π) β β€} β
(β€β₯β1) β§ {π β β β£ ((π΅βπ) Β· π) β β€} β β
) β
inf({π β β
β£ ((π΅βπ) Β· π) β β€}, β, < ) β
{π β β β£
((π΅βπ) Β· π) β β€}) |
44 | 31, 42, 43 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β
inf({π β β
β£ ((π΅βπ) Β· π) β β€}, β, < ) β
{π β β β£
((π΅βπ) Β· π) β β€}) |
45 | 29, 44 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β (πβπ) β {π β β β£ ((π΅βπ) Β· π) β β€}) |
46 | 19, 45 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β (πβπ) β β) |
47 | | nnmulcl 12184 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (π Β· π) β β) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β β)) β (π Β· π) β β) |
49 | 17, 18, 46, 48 | seqf 13936 |
. . . . . . . . . . . . 13
β’ (π β seq0( Β· , π):β0βΆβ) |
50 | | dgrcl 25610 |
. . . . . . . . . . . . . 14
β’ (πΉ β (Polyββ)
β (degβπΉ) β
β0) |
51 | 11, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (degβπΉ) β
β0) |
52 | 49, 51 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (π β (seq0( Β· , π)β(degβπΉ)) β
β) |
53 | 4, 52 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ (π β π
β β) |
54 | 53 | nncnd 12176 |
. . . . . . . . . 10
β’ (π β π
β β) |
55 | 54 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β π
β β) |
56 | | elfznn0 13541 |
. . . . . . . . . 10
β’ (π β (0...(degβπΉ)) β π β β0) |
57 | 35 | coef3 25609 |
. . . . . . . . . . . . . 14
β’ (πΉ β (Polyββ)
β π΅:β0βΆβ) |
58 | 11, 57 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅:β0βΆβ) |
59 | 58 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β π΅:β0βΆβ) |
60 | 59 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β β0) β (π΅βπ) β β) |
61 | | expcl 13992 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π β β0)
β (π§βπ) β
β) |
62 | 61 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β β0) β (π§βπ) β β) |
63 | 60, 62 | mulcld 11182 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β ((π΅βπ) Β· (π§βπ)) β β) |
64 | 56, 63 | sylan2 594 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β (0...(degβπΉ))) β ((π΅βπ) Β· (π§βπ)) β β) |
65 | 16, 55, 64 | fsummulc2 15676 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (π
Β· Ξ£π β (0...(degβπΉ))((π΅βπ) Β· (π§βπ))) = Ξ£π β (0...(degβπΉ))(π
Β· ((π΅βπ) Β· (π§βπ)))) |
66 | | eqid 2737 |
. . . . . . . . . . 11
β’
(degβπΉ) =
(degβπΉ) |
67 | 35, 66 | coeid2 25616 |
. . . . . . . . . 10
β’ ((πΉ β (Polyββ)
β§ π§ β β)
β (πΉβπ§) = Ξ£π β (0...(degβπΉ))((π΅βπ) Β· (π§βπ))) |
68 | 11, 67 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β (πΉβπ§) = Ξ£π β (0...(degβπΉ))((π΅βπ) Β· (π§βπ))) |
69 | 68 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (π
Β· (πΉβπ§)) = (π
Β· Ξ£π β (0...(degβπΉ))((π΅βπ) Β· (π§βπ)))) |
70 | 55 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β β0) β π
β
β) |
71 | 70, 60, 62 | mulassd 11185 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β ((π
Β· (π΅βπ)) Β· (π§βπ)) = (π
Β· ((π΅βπ) Β· (π§βπ)))) |
72 | 56, 71 | sylan2 594 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β (0...(degβπΉ))) β ((π
Β· (π΅βπ)) Β· (π§βπ)) = (π
Β· ((π΅βπ) Β· (π§βπ)))) |
73 | 72 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π§ β β) β Ξ£π β (0...(degβπΉ))((π
Β· (π΅βπ)) Β· (π§βπ)) = Ξ£π β (0...(degβπΉ))(π
Β· ((π΅βπ) Β· (π§βπ)))) |
74 | 65, 69, 73 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π β§ π§ β β) β (π
Β· (πΉβπ§)) = Ξ£π β (0...(degβπΉ))((π
Β· (π΅βπ)) Β· (π§βπ))) |
75 | 74 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π§ β β β¦ (π
Β· (πΉβπ§))) = (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π
Β· (π΅βπ)) Β· (π§βπ)))) |
76 | 15, 75 | eqtrd 2777 |
. . . . 5
β’ (π β ((β Γ {π
}) βf Β·
πΉ) = (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π
Β· (π΅βπ)) Β· (π§βπ)))) |
77 | | zsscn 12514 |
. . . . . . 7
β’ β€
β β |
78 | 77 | a1i 11 |
. . . . . 6
β’ (π β β€ β
β) |
79 | 54 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π
β
β) |
80 | 46 | nncnd 12176 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πβπ) β β) |
81 | 46 | nnne0d 12210 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (πβπ) β 0) |
82 | 79, 80, 81 | divcan2d 11940 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((πβπ) Β· (π
/ (πβπ))) = π
) |
83 | 82 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π΅βπ) Β· ((πβπ) Β· (π
/ (πβπ)))) = ((π΅βπ) Β· π
)) |
84 | 58 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π΅βπ) β β) |
85 | 79, 80, 81 | divcld 11938 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π
/ (πβπ)) β β) |
86 | 84, 80, 85 | mulassd 11185 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (((π΅βπ) Β· (πβπ)) Β· (π
/ (πβπ))) = ((π΅βπ) Β· ((πβπ) Β· (π
/ (πβπ))))) |
87 | 79, 84 | mulcomd 11183 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π
Β· (π΅βπ)) = ((π΅βπ) Β· π
)) |
88 | 83, 86, 87 | 3eqtr4rd 2788 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π
Β· (π΅βπ)) = (((π΅βπ) Β· (πβπ)) Β· (π
/ (πβπ)))) |
89 | 56, 88 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β (π
Β· (π΅βπ)) = (((π΅βπ) Β· (πβπ)) Β· (π
/ (πβπ)))) |
90 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π΅βπ) Β· π) = ((π΅βπ) Β· (πβπ))) |
91 | 90 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (((π΅βπ) Β· π) β β€ β ((π΅βπ) Β· (πβπ)) β β€)) |
92 | 91 | elrab 3650 |
. . . . . . . . . . 11
β’ ((πβπ) β {π β β β£ ((π΅βπ) Β· π) β β€} β ((πβπ) β β β§ ((π΅βπ) Β· (πβπ)) β β€)) |
93 | 92 | simprbi 498 |
. . . . . . . . . 10
β’ ((πβπ) β {π β β β£ ((π΅βπ) Β· π) β β€} β ((π΅βπ) Β· (πβπ)) β β€) |
94 | 45, 93 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π΅βπ) Β· (πβπ)) β β€) |
95 | 56, 94 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β ((π΅βπ) Β· (πβπ)) β β€) |
96 | | elqaa.3 |
. . . . . . . . . 10
β’ (π β (πΉβπ΄) = 0) |
97 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β V, π¦ β V β¦ ((π₯ Β· π¦) mod (πβπ))) = (π₯ β V, π¦ β V β¦ ((π₯ Β· π¦) mod (πβπ))) |
98 | 1, 10, 96, 35, 25, 4, 97 | elqaalem2 25696 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β (π
mod (πβπ)) = 0) |
99 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(degβπΉ))) β π
β β) |
100 | 56, 46 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β β) |
101 | | nnre 12167 |
. . . . . . . . . . 11
β’ (π
β β β π
β
β) |
102 | | nnrp 12933 |
. . . . . . . . . . 11
β’ ((πβπ) β β β (πβπ) β
β+) |
103 | | mod0 13788 |
. . . . . . . . . . 11
β’ ((π
β β β§ (πβπ) β β+) β ((π
mod (πβπ)) = 0 β (π
/ (πβπ)) β β€)) |
104 | 101, 102,
103 | syl2an 597 |
. . . . . . . . . 10
β’ ((π
β β β§ (πβπ) β β) β ((π
mod (πβπ)) = 0 β (π
/ (πβπ)) β β€)) |
105 | 99, 100, 104 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β ((π
mod (πβπ)) = 0 β (π
/ (πβπ)) β β€)) |
106 | 98, 105 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (π
/ (πβπ)) β β€) |
107 | 95, 106 | zmulcld 12620 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β (((π΅βπ) Β· (πβπ)) Β· (π
/ (πβπ))) β β€) |
108 | 89, 107 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β (π
Β· (π΅βπ)) β β€) |
109 | 78, 51, 108 | elplyd 25579 |
. . . . 5
β’ (π β (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π
Β· (π΅βπ)) Β· (π§βπ))) β
(Polyββ€)) |
110 | 76, 109 | eqeltrd 2838 |
. . . 4
β’ (π β ((β Γ {π
}) βf Β·
πΉ) β
(Polyββ€)) |
111 | | eldifsn 4752 |
. . . . . . 7
β’ (πΉ β ((Polyββ)
β {0π}) β (πΉ β (Polyββ) β§ πΉ β
0π)) |
112 | 10, 111 | sylib 217 |
. . . . . 6
β’ (π β (πΉ β (Polyββ) β§ πΉ β
0π)) |
113 | 112 | simprd 497 |
. . . . 5
β’ (π β πΉ β
0π) |
114 | | oveq1 7369 |
. . . . . . 7
β’
(((β Γ {π
}) βf Β· πΉ) = 0π β
(((β Γ {π
})
βf Β· πΉ) βf / (β Γ
{π
})) =
(0π βf / (β Γ {π
}))) |
115 | 13 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β (πΉβπ§) β β) |
116 | 53 | nnne0d 12210 |
. . . . . . . . . . . 12
β’ (π β π
β 0) |
117 | 116 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β π
β 0) |
118 | 115, 55, 117 | divcan3d 11943 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β ((π
Β· (πΉβπ§)) / π
) = (πΉβπ§)) |
119 | 118 | mpteq2dva 5210 |
. . . . . . . . 9
β’ (π β (π§ β β β¦ ((π
Β· (πΉβπ§)) / π
)) = (π§ β β β¦ (πΉβπ§))) |
120 | | ovexd 7397 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β (π
Β· (πΉβπ§)) β V) |
121 | 3, 120, 6, 15, 9 | offval2 7642 |
. . . . . . . . 9
β’ (π β (((β Γ {π
}) βf Β·
πΉ) βf /
(β Γ {π
})) =
(π§ β β β¦
((π
Β· (πΉβπ§)) / π
))) |
122 | 119, 121,
14 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (π β (((β Γ {π
}) βf Β·
πΉ) βf /
(β Γ {π
})) =
πΉ) |
123 | 54, 116 | div0d 11937 |
. . . . . . . . . 10
β’ (π β (0 / π
) = 0) |
124 | 123 | mpteq2dv 5212 |
. . . . . . . . 9
β’ (π β (π§ β β β¦ (0 / π
)) = (π§ β β β¦ 0)) |
125 | | 0cnd 11155 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β 0 β
β) |
126 | | df-0p 25050 |
. . . . . . . . . . . 12
β’
0π = (β Γ {0}) |
127 | | fconstmpt 5699 |
. . . . . . . . . . . 12
β’ (β
Γ {0}) = (π§ β
β β¦ 0) |
128 | 126, 127 | eqtri 2765 |
. . . . . . . . . . 11
β’
0π = (π§ β β β¦ 0) |
129 | 128 | a1i 11 |
. . . . . . . . . 10
β’ (π β 0π =
(π§ β β β¦
0)) |
130 | 3, 125, 6, 129, 9 | offval2 7642 |
. . . . . . . . 9
β’ (π β (0π
βf / (β Γ {π
})) = (π§ β β β¦ (0 / π
))) |
131 | 124, 130,
129 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (π β (0π
βf / (β Γ {π
})) =
0π) |
132 | 122, 131 | eqeq12d 2753 |
. . . . . . 7
β’ (π β ((((β Γ {π
}) βf Β·
πΉ) βf /
(β Γ {π
})) =
(0π βf / (β Γ {π
})) β πΉ = 0π)) |
133 | 114, 132 | imbitrid 243 |
. . . . . 6
β’ (π β (((β Γ {π
}) βf Β·
πΉ) = 0π
β πΉ =
0π)) |
134 | 133 | necon3d 2965 |
. . . . 5
β’ (π β (πΉ β 0π β ((β
Γ {π
})
βf Β· πΉ) β
0π)) |
135 | 113, 134 | mpd 15 |
. . . 4
β’ (π β ((β Γ {π
}) βf Β·
πΉ) β
0π) |
136 | | eldifsn 4752 |
. . . 4
β’
(((β Γ {π
}) βf Β· πΉ) β ((Polyββ€)
β {0π}) β (((β Γ {π
}) βf Β· πΉ) β (Polyββ€)
β§ ((β Γ {π
}) βf Β· πΉ) β
0π)) |
137 | 110, 135,
136 | sylanbrc 584 |
. . 3
β’ (π β ((β Γ {π
}) βf Β·
πΉ) β
((Polyββ€) β {0π})) |
138 | 5 | fconst 6733 |
. . . . . . 7
β’ (β
Γ {π
}):ββΆ{π
} |
139 | | ffn 6673 |
. . . . . . 7
β’ ((β
Γ {π
}):ββΆ{π
} β (β Γ {π
}) Fn β) |
140 | 138, 139 | mp1i 13 |
. . . . . 6
β’ (π β (β Γ {π
}) Fn β) |
141 | 13 | ffnd 6674 |
. . . . . 6
β’ (π β πΉ Fn β) |
142 | | inidm 4183 |
. . . . . 6
β’ (β
β© β) = β |
143 | 5 | fvconst2 7158 |
. . . . . . 7
β’ (π΄ β β β ((β
Γ {π
})βπ΄) = π
) |
144 | 143 | adantl 483 |
. . . . . 6
β’ ((π β§ π΄ β β) β ((β Γ
{π
})βπ΄) = π
) |
145 | 96 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β β) β (πΉβπ΄) = 0) |
146 | 140, 141,
3, 3, 142, 144, 145 | ofval 7633 |
. . . . 5
β’ ((π β§ π΄ β β) β (((β Γ
{π
}) βf
Β· πΉ)βπ΄) = (π
Β· 0)) |
147 | 1, 146 | mpdan 686 |
. . . 4
β’ (π β (((β Γ {π
}) βf Β·
πΉ)βπ΄) = (π
Β· 0)) |
148 | 54 | mul01d 11361 |
. . . 4
β’ (π β (π
Β· 0) = 0) |
149 | 147, 148 | eqtrd 2777 |
. . 3
β’ (π β (((β Γ {π
}) βf Β·
πΉ)βπ΄) = 0) |
150 | | fveq1 6846 |
. . . . 5
β’ (π = ((β Γ {π
}) βf Β·
πΉ) β (πβπ΄) = (((β Γ {π
}) βf Β· πΉ)βπ΄)) |
151 | 150 | eqeq1d 2739 |
. . . 4
β’ (π = ((β Γ {π
}) βf Β·
πΉ) β ((πβπ΄) = 0 β (((β Γ {π
}) βf Β·
πΉ)βπ΄) = 0)) |
152 | 151 | rspcev 3584 |
. . 3
β’
((((β Γ {π
}) βf Β· πΉ) β ((Polyββ€)
β {0π}) β§ (((β Γ {π
}) βf Β· πΉ)βπ΄) = 0) β βπ β ((Polyββ€) β
{0π})(πβπ΄) = 0) |
153 | 137, 149,
152 | syl2anc 585 |
. 2
β’ (π β βπ β ((Polyββ€) β
{0π})(πβπ΄) = 0) |
154 | | elaa 25692 |
. 2
β’ (π΄ β πΈ β (π΄ β β β§
βπ β
((Polyββ€) β {0π})(πβπ΄) = 0)) |
155 | 1, 153, 154 | sylanbrc 584 |
1
β’ (π β π΄ β πΈ) |