irngnzply1lem

Description: In the case of a field E , a root X of some nonzero polynomial P with coefficients in a subfield F is integral over F . (Contributed by Thierry Arnoux, 5-Feb-2025)

	Ref	Expression
Hypotheses	irngnzply1.o	\|- O = ( E evalSub1 F )
	irngnzply1.z	\|- Z = ( 0g ` ( Poly1 ` E ) )
	irngnzply1.1	\|- .0. = ( 0g ` E )
	irngnzply1.e	\|- ( ph -> E e. Field )
	irngnzply1.f	\|- ( ph -> F e. ( SubDRing ` E ) )
	irngnzply1lem.b	\|- B = ( Base ` E )
	irngnzply1lem.1	\|- ( ph -> P e. dom O )
	irngnzply1lem.2	\|- ( ph -> P =/= Z )
	irngnzply1lem.3	\|- ( ph -> ( ( O ` P ) ` X ) = .0. )
	irngnzply1lem.x	\|- ( ph -> X e. B )
Assertion	irngnzply1lem	\|- ( ph -> X e. ( E IntgRing F ) )

Proof

Step	Hyp	Ref	Expression
1		irngnzply1.o	\|- O = ( E evalSub1 F )
2		irngnzply1.z	\|- Z = ( 0g ` ( Poly1 ` E ) )
3		irngnzply1.1	\|- .0. = ( 0g ` E )
4		irngnzply1.e	\|- ( ph -> E e. Field )
5		irngnzply1.f	\|- ( ph -> F e. ( SubDRing ` E ) )
6		irngnzply1lem.b	\|- B = ( Base ` E )
7		irngnzply1lem.1	\|- ( ph -> P e. dom O )
8		irngnzply1lem.2	\|- ( ph -> P =/= Z )
9		irngnzply1lem.3	\|- ( ph -> ( ( O ` P ) ` X ) = .0. )
10		irngnzply1lem.x	\|- ( ph -> X e. B )
11		issdrg	\|- ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E \|`s F ) e. DivRing ) )
12	11	simp3bi	\|- ( F e. ( SubDRing ` E ) -> ( E \|`s F ) e. DivRing )
13	5 12	syl	\|- ( ph -> ( E \|`s F ) e. DivRing )
14	13	drngringd	\|- ( ph -> ( E \|`s F ) e. Ring )
15	4	fldcrngd	\|- ( ph -> E e. CRing )
16	5 11	sylib	\|- ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E \|`s F ) e. DivRing ) )
17	16	simp2d	\|- ( ph -> F e. ( SubRing ` E ) )
18		eqid	\|- ( E ^s B ) = ( E ^s B )
19		eqid	\|- ( E \|`s F ) = ( E \|`s F )
20		eqid	\|- ( Poly1 ` ( E \|`s F ) ) = ( Poly1 ` ( E \|`s F ) )
21	1 6 18 19 20	evls1rhm	\|- ( ( E e. CRing /\ F e. ( SubRing ` E ) ) -> O e. ( ( Poly1 ` ( E \|`s F ) ) RingHom ( E ^s B ) ) )
22	15 17 21	syl2anc	\|- ( ph -> O e. ( ( Poly1 ` ( E \|`s F ) ) RingHom ( E ^s B ) ) )
23		eqid	\|- ( Base ` ( Poly1 ` ( E \|`s F ) ) ) = ( Base ` ( Poly1 ` ( E \|`s F ) ) )
24		eqid	\|- ( Base ` ( E ^s B ) ) = ( Base ` ( E ^s B ) )
25	23 24	rhmf	\|- ( O e. ( ( Poly1 ` ( E \|`s F ) ) RingHom ( E ^s B ) ) -> O : ( Base ` ( Poly1 ` ( E \|`s F ) ) ) --> ( Base ` ( E ^s B ) ) )
26	22 25	syl	\|- ( ph -> O : ( Base ` ( Poly1 ` ( E \|`s F ) ) ) --> ( Base ` ( E ^s B ) ) )
27	26	fdmd	\|- ( ph -> dom O = ( Base ` ( Poly1 ` ( E \|`s F ) ) ) )
28	7 27	eleqtrd	\|- ( ph -> P e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) )
29		eqid	\|- ( Poly1 ` E ) = ( Poly1 ` E )
30	29 19 20 23 17 2	ressply10g	\|- ( ph -> Z = ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) )
31	8 30	neeqtrd	\|- ( ph -> P =/= ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) )
32		eqid	\|- ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) = ( 0g ` ( Poly1 ` ( E \|`s F ) ) )
33		eqid	\|- ( Unic1p ` ( E \|`s F ) ) = ( Unic1p ` ( E \|`s F ) )
34	20 23 32 33	drnguc1p	\|- ( ( ( E \|`s F ) e. DivRing /\ P e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) ) -> P e. ( Unic1p ` ( E \|`s F ) ) )
35	13 28 31 34	syl3anc	\|- ( ph -> P e. ( Unic1p ` ( E \|`s F ) ) )
36		eqid	\|- ( Monic1p ` ( E \|`s F ) ) = ( Monic1p ` ( E \|`s F ) )
37		eqid	\|- ( .r ` ( Poly1 ` ( E \|`s F ) ) ) = ( .r ` ( Poly1 ` ( E \|`s F ) ) )
38		eqid	\|- ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) = ( algSc ` ( Poly1 ` ( E \|`s F ) ) )
39		eqid	\|- ( deg1 ` ( E \|`s F ) ) = ( deg1 ` ( E \|`s F ) )
40		eqid	\|- ( invr ` ( E \|`s F ) ) = ( invr ` ( E \|`s F ) )
41	33 36 20 37 38 39 40	uc1pmon1p	\|- ( ( ( E \|`s F ) e. Ring /\ P e. ( Unic1p ` ( E \|`s F ) ) ) -> ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) e. ( Monic1p ` ( E \|`s F ) ) )
42	14 35 41	syl2anc	\|- ( ph -> ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) e. ( Monic1p ` ( E \|`s F ) ) )
43		simpr	\|- ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) -> p = ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) )
44	43	fveq2d	\|- ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) -> ( O ` p ) = ( O ` ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) )
45	44	fveq1d	\|- ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) -> ( ( O ` p ) ` X ) = ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) ` X ) )
46	45	eqeq1d	\|- ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) -> ( ( ( O ` p ) ` X ) = .0. <-> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) ` X ) = .0. ) )
47		eqid	\|- ( .r ` E ) = ( .r ` E )
48		eqid	\|- ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) = ( Scalar ` ( Poly1 ` ( E \|`s F ) ) )
49		fldsdrgfld	\|- ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E \|`s F ) e. Field )
50	4 5 49	syl2anc	\|- ( ph -> ( E \|`s F ) e. Field )
51	50	fldcrngd	\|- ( ph -> ( E \|`s F ) e. CRing )
52	20	ply1assa	\|- ( ( E \|`s F ) e. CRing -> ( Poly1 ` ( E \|`s F ) ) e. AssAlg )
53	51 52	syl	\|- ( ph -> ( Poly1 ` ( E \|`s F ) ) e. AssAlg )
54		assaring	\|- ( ( Poly1 ` ( E \|`s F ) ) e. AssAlg -> ( Poly1 ` ( E \|`s F ) ) e. Ring )
55	53 54	syl	\|- ( ph -> ( Poly1 ` ( E \|`s F ) ) e. Ring )
56	20	ply1lmod	\|- ( ( E \|`s F ) e. Ring -> ( Poly1 ` ( E \|`s F ) ) e. LMod )
57	14 56	syl	\|- ( ph -> ( Poly1 ` ( E \|`s F ) ) e. LMod )
58		eqid	\|- ( Base ` ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) )
59	38 48 55 57 58 23	asclf	\|- ( ph -> ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) : ( Base ` ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) ) --> ( Base ` ( Poly1 ` ( E \|`s F ) ) ) )
60		eqid	\|- ( Base ` ( E \|`s F ) ) = ( Base ` ( E \|`s F ) )
61		eqid	\|- ( 0g ` ( E \|`s F ) ) = ( 0g ` ( E \|`s F ) )
62	39 20 32 23	deg1nn0cl	\|- ( ( ( E \|`s F ) e. Ring /\ P e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) ) -> ( ( deg1 ` ( E \|`s F ) ) ` P ) e. NN0 )
63	14 28 31 62	syl3anc	\|- ( ph -> ( ( deg1 ` ( E \|`s F ) ) ` P ) e. NN0 )
64		eqid	\|- ( coe1 ` P ) = ( coe1 ` P )
65	64 23 20 60	coe1fvalcl	\|- ( ( P e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) /\ ( ( deg1 ` ( E \|`s F ) ) ` P ) e. NN0 ) -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) e. ( Base ` ( E \|`s F ) ) )
66	28 63 65	syl2anc	\|- ( ph -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) e. ( Base ` ( E \|`s F ) ) )
67	39 20 32 23 61 64	deg1ldg	\|- ( ( ( E \|`s F ) e. Ring /\ P e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E \|`s F ) ) ) ) -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) =/= ( 0g ` ( E \|`s F ) ) )
68	14 28 31 67	syl3anc	\|- ( ph -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) =/= ( 0g ` ( E \|`s F ) ) )
69	60 61 40 13 66 68	drnginvrcld	\|- ( ph -> ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) e. ( Base ` ( E \|`s F ) ) )
70	20	ply1sca	\|- ( ( E \|`s F ) e. Field -> ( E \|`s F ) = ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) )
71	50 70	syl	\|- ( ph -> ( E \|`s F ) = ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) )
72	71	fveq2d	\|- ( ph -> ( Base ` ( E \|`s F ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) ) )
73	69 72	eleqtrd	\|- ( ph -> ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) e. ( Base ` ( Scalar ` ( Poly1 ` ( E \|`s F ) ) ) ) )
74	59 73	ffvelcdmd	\|- ( ph -> ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) e. ( Base ` ( Poly1 ` ( E \|`s F ) ) ) )
75	1 6 20 19 23 37 47 15 17 74 28 10	evls1muld	\|- ( ph -> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) ` X ) = ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) ( ( O ` P ) ` X ) ) )
76	9	oveq2d	\|- ( ph -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) ( ( O ` P ) ` X ) ) = ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) )
77	15	crngringd	\|- ( ph -> E e. Ring )
78	6	fvexi	\|- B e. _V
79	78	a1i	\|- ( ph -> B e. _V )
80	26 74	ffvelcdmd	\|- ( ph -> ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) e. ( Base ` ( E ^s B ) ) )
81	18 6 24 4 79 80	pwselbas	\|- ( ph -> ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) : B --> B )
82	81 10	ffvelcdmd	\|- ( ph -> ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) e. B )
83	6 47 3	ringrz	\|- ( ( E e. Ring /\ ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) e. B ) -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) = .0. )
84	77 82 83	syl2anc	\|- ( ph -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) = .0. )
85	75 76 84	3eqtrd	\|- ( ph -> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E \|`s F ) ) ) ` ( ( invr ` ( E \|`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E \|`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E \|`s F ) ) ) P ) ) ` X ) = .0. )
86	42 46 85	rspcedvd	\|- ( ph -> E. p e. ( Monic1p ` ( E \|`s F ) ) ( ( O ` p ) ` X ) = .0. )
87	1 19 6 3 15 17	elirng	\|- ( ph -> ( X e. ( E IntgRing F ) <-> ( X e. B /\ E. p e. ( Monic1p ` ( E \|`s F ) ) ( ( O ` p ) ` X ) = .0. ) ) )
88	10 86 87	mpbir2and	\|- ( ph -> X e. ( E IntgRing F ) )

Metamath Proof Explorer

Theorem irngnzply1lem

Proof