Theorem ply1annprmidl

Description: The set Q of polynomials annihilating an element A is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025)

	Ref	Expression
Hypotheses	ply1annig1p.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
	ply1annig1p.p	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
	ply1annig1p.b	$$⊢B={\mathrm{Base}}_E$$
	ply1annig1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
	ply1annig1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	ply1annig1p.a	$$⊢\phi \to A\in B$$
	ply1annig1p.0	$$⊢\underset{\dot{}}{0}=0_E$$
	ply1annig1p.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
Assertion	ply1annprmidl	Could not format assertion : No typesetting found for |- ( ph -> Q e. ( PrmIdeal ` P ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ply1annig1p.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
2		ply1annig1p.p	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
3		ply1annig1p.b	$$⊢B={\mathrm{Base}}_E$$
4		ply1annig1p.e	$$⊢\phi \to E\in \mathrm{Field}$$
5		ply1annig1p.f	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
6		ply1annig1p.a	$$⊢\phi \to A\in B$$
7		ply1annig1p.0	$$⊢\underset{\dot{}}{0}=0_E$$
8		ply1annig1p.q	$$⊢Q=\left\{q\in \mathrm{dom}O|O\left(q\right)\left(A\right)=\underset{\dot{}}{0}\right\}$$
9	4	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
10		issdrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\leftrightarrow \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
11	5 10	sylib	$$⊢\phi \to \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
12	11	simp2d	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
13		eqid	$$⊢\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)=\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)$$
14	1 2 3 9 12 6 7 8 13	ply1annidllem	$$⊢\phi \to Q={\left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
15		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
16	1 2 3 15 9 12 6 13	evls1maprhm	$$⊢\phi \to \left(p\in {\mathrm{Base}}_P⟼O\left(p\right)\left(A\right)\right)\in \left(P\mathrm{RingHom}E\right)$$
17		fldidom	$$⊢E\in \mathrm{Field}\to E\in \mathrm{IDomn}$$
18	7	prmidl0	Could not format ( ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) <-> E e. IDomn ) : No typesetting found for |- ( ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) <-> E e. IDomn ) with typecode |-
19	18	biimpri	Could not format ( E e. IDomn -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) ) : No typesetting found for |- ( E e. IDomn -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) ) with typecode |-
20	4 17 19	3syl	Could not format ( ph -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) ) : No typesetting found for |- ( ph -> ( E e. CRing /\ { .0. } e. ( PrmIdeal ` E ) ) ) with typecode |-
21	20	simprd	Could not format ( ph -> { .0. } e. ( PrmIdeal ` E ) ) : No typesetting found for |- ( ph -> { .0. } e. ( PrmIdeal ` E ) ) with typecode |-
22		eqid	Could not format ( PrmIdeal ` P ) = ( PrmIdeal ` P ) : No typesetting found for |- ( PrmIdeal ` P ) = ( PrmIdeal ` P ) with typecode |-
23	22	rhmpreimaprmidl	Could not format ( ( ( E e. CRing /\ ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom E ) ) /\ { .0. } e. ( PrmIdeal ` E ) ) -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) ) : No typesetting found for |- ( ( ( E e. CRing /\ ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) e. ( P RingHom E ) ) /\ { .0. } e. ( PrmIdeal ` E ) ) -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) ) with typecode |-
24	9 16 21 23	syl21anc	Could not format ( ph -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) ) : No typesetting found for |- ( ph -> ( `' ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) ) " { .0. } ) e. ( PrmIdeal ` P ) ) with typecode |-
25	14 24	eqeltrd	Could not format ( ph -> Q e. ( PrmIdeal ` P ) ) : No typesetting found for |- ( ph -> Q e. ( PrmIdeal ` P ) ) with typecode |-