Theorem 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	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	irngnzply1.z	⊢ 𝑍 = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
	irngnzply1.1	⊢ 0 = ( 0g ‘ 𝐸 )
	irngnzply1.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	irngnzply1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	irngnzply1lem.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	irngnzply1lem.1	⊢ ( 𝜑 → 𝑃 ∈ dom 𝑂 )
	irngnzply1lem.2	⊢ ( 𝜑 → 𝑃 ≠ 𝑍 )
	irngnzply1lem.3	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑃 ) ‘ 𝑋 ) = 0 )
	irngnzply1lem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	irngnzply1lem	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 IntgRing 𝐹 ) )

Proof

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