This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) )