Step | Hyp | Ref
| Expression |
1 | | facth.1 |
. . . . 5
β’ πΊ = (Xp
βf β (β Γ {π΄})) |
2 | | eqid 2732 |
. . . . 5
β’ (πΉ βf β
(πΊ βf
Β· (πΉ quot πΊ))) = (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) |
3 | 1, 2 | plyrem 25809 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π΄ β β) β (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) = (β Γ {(πΉβπ΄)})) |
4 | 3 | 3adant3 1132 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) = (β Γ {(πΉβπ΄)})) |
5 | | simp3 1138 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΉβπ΄) = 0) |
6 | 5 | sneqd 4639 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β {(πΉβπ΄)} = {0}) |
7 | 6 | xpeq2d 5705 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (β Γ {(πΉβπ΄)}) = (β Γ
{0})) |
8 | 4, 7 | eqtrd 2772 |
. 2
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) = (β Γ
{0})) |
9 | | cnex 11187 |
. . . 4
β’ β
β V |
10 | 9 | a1i 11 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β β β
V) |
11 | | simp1 1136 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΉ β (Polyβπ)) |
12 | | plyf 25703 |
. . . 4
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
13 | 11, 12 | syl 17 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΉ:ββΆβ) |
14 | 1 | plyremlem 25808 |
. . . . . . 7
β’ (π΄ β β β (πΊ β (Polyββ)
β§ (degβπΊ) = 1
β§ (β‘πΊ β {0}) = {π΄})) |
15 | 14 | 3ad2ant2 1134 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΊ β (Polyββ) β§
(degβπΊ) = 1 β§
(β‘πΊ β {0}) = {π΄})) |
16 | 15 | simp1d 1142 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΊ β
(Polyββ)) |
17 | | plyssc 25705 |
. . . . . . 7
β’
(Polyβπ)
β (Polyββ) |
18 | 17, 11 | sselid 3979 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΉ β
(Polyββ)) |
19 | 15 | simp2d 1143 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (degβπΊ) = 1) |
20 | | ax-1ne0 11175 |
. . . . . . . . 9
β’ 1 β
0 |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β 1 β 0) |
22 | 19, 21 | eqnetrd 3008 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (degβπΊ) β 0) |
23 | | fveq2 6888 |
. . . . . . . . 9
β’ (πΊ = 0π β
(degβπΊ) =
(degβ0π)) |
24 | | dgr0 25767 |
. . . . . . . . 9
β’
(degβ0π) = 0 |
25 | 23, 24 | eqtrdi 2788 |
. . . . . . . 8
β’ (πΊ = 0π β
(degβπΊ) =
0) |
26 | 25 | necon3i 2973 |
. . . . . . 7
β’
((degβπΊ) β
0 β πΊ β
0π) |
27 | 22, 26 | syl 17 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΊ β
0π) |
28 | | quotcl2 25806 |
. . . . . 6
β’ ((πΉ β (Polyββ)
β§ πΊ β
(Polyββ) β§ πΊ β 0π) β (πΉ quot πΊ) β
(Polyββ)) |
29 | 18, 16, 27, 28 | syl3anc 1371 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΉ quot πΊ) β
(Polyββ)) |
30 | | plymulcl 25726 |
. . . . 5
β’ ((πΊ β (Polyββ)
β§ (πΉ quot πΊ) β (Polyββ))
β (πΊ
βf Β· (πΉ quot πΊ)) β
(Polyββ)) |
31 | 16, 29, 30 | syl2anc 584 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΊ βf Β· (πΉ quot πΊ)) β
(Polyββ)) |
32 | | plyf 25703 |
. . . 4
β’ ((πΊ βf Β·
(πΉ quot πΊ)) β (Polyββ) β (πΊ βf Β·
(πΉ quot πΊ)):ββΆβ) |
33 | 31, 32 | syl 17 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β (πΊ βf Β· (πΉ quot πΊ)):ββΆβ) |
34 | | ofsubeq0 12205 |
. . 3
β’ ((β
β V β§ πΉ:ββΆβ β§ (πΊ βf Β·
(πΉ quot πΊ)):ββΆβ) β ((πΉ βf β
(πΊ βf
Β· (πΉ quot πΊ))) = (β Γ {0})
β πΉ = (πΊ βf Β·
(πΉ quot πΊ)))) |
35 | 10, 13, 33, 34 | syl3anc 1371 |
. 2
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β ((πΉ βf β (πΊ βf Β·
(πΉ quot πΊ))) = (β Γ {0}) β πΉ = (πΊ βf Β· (πΉ quot πΊ)))) |
36 | 8, 35 | mpbid 231 |
1
β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΉ = (πΊ βf Β· (πΉ quot πΊ))) |