irngnminplynz

Description: Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	irngnminplynz.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
	irngnminplynz.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	irngnminplynz.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	irngnminplynz.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	irngnminplynz.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
Assertion	irngnminplynz	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		irngnminplynz.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
2		irngnminplynz.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
3		irngnminplynz.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
4		irngnminplynz.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5		irngnminplynz.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
6		sdrgsubrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
7	3 6	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
8		eqid	⊢ ( 𝐸 ↾_s 𝐹 ) = ( 𝐸 ↾_s 𝐹 )
9	8	subrgring	⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( 𝐸 ↾_s 𝐹 ) ∈ Ring )
10	7 9	syl	⊢ ( 𝜑 → ( 𝐸 ↾_s 𝐹 ) ∈ Ring )
11		eqid	⊢ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
12	11	ply1ring	⊢ ( ( 𝐸 ↾_s 𝐹 ) ∈ Ring → ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring )
13	10 12	syl	⊢ ( 𝜑 → ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring )
14		eqid	⊢ ( 𝐸 evalSub₁ 𝐹 ) = ( 𝐸 evalSub₁ 𝐹 )
15		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
16	2	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
17		eqid	⊢ ( 0_g ‘ 𝐸 ) = ( 0_g ‘ 𝐸 )
18	14 8 15 17 16 7	irngssv	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
19	18 5	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
20		eqid	⊢ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } = { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) }
21	14 11 15 16 7 19 17 20	ply1annidl	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∈ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
22		eqid	⊢ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
23		eqid	⊢ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
24	22 23	lidlss	⊢ ( { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∈ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ⊆ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
25	21 24	syl	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ⊆ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
26	8	sdrgdrng	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾_s 𝐹 ) ∈ DivRing )
27	3 26	syl	⊢ ( 𝜑 → ( 𝐸 ↾_s 𝐹 ) ∈ DivRing )
28		eqid	⊢ ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
29	11 28 23	ig1pcl	⊢ ( ( ( 𝐸 ↾_s 𝐹 ) ∈ DivRing ∧ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∈ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ) → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } )
30	27 21 29	syl2anc	⊢ ( 𝜑 → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } )
31	25 30	sseldd	⊢ ( 𝜑 → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
32		eqid	⊢ ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
33	14 11 15 2 3 19 17 20 32 28	ply1annig1p	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } = ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) )
34		fveq2	⊢ ( 𝑞 = 𝑝 → ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) = ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) )
35	34	fveq1d	⊢ ( 𝑞 = 𝑝 → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) )
36	35	eqeq1d	⊢ ( 𝑞 = 𝑝 → ( ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) ↔ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) ) )
37		simplr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) )
38	37	eldifad	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) )
39	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝐸 ∈ CRing )
40	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
41	14 11 22 16 7	evls1dm	⊢ ( 𝜑 → dom ( 𝐸 evalSub₁ 𝐹 ) = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
42	41	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → dom ( 𝐸 evalSub₁ 𝐹 ) = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
43	38 42	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
44	14 11 22 39 40 15 43	evls1fvf	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐸 ) )
45	44	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) )
46		elpreima	⊢ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) → ( 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ↔ ( 𝐴 ∈ ( Base ‘ 𝐸 ) ∧ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) ∈ { ( 0_g ‘ 𝐸 ) } ) ) )
47	46	simplbda	⊢ ( ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) ∈ { ( 0_g ‘ 𝐸 ) } )
48	45 47	sylancom	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) ∈ { ( 0_g ‘ 𝐸 ) } )
49		elsni	⊢ ( ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) ∈ { ( 0_g ‘ 𝐸 ) } → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) )
50	48 49	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) )
51	36 38 50	elrabd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } )
52		eldifsni	⊢ ( 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) → 𝑝 ≠ 𝑍 )
53	37 52	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ≠ 𝑍 )
54		eqid	⊢ ( Poly₁ ‘ 𝐸 ) = ( Poly₁ ‘ 𝐸 )
55	54 8 11 22 7 1	ressply10g	⊢ ( 𝜑 → 𝑍 = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
56	55	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑍 = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
57	53 56	neeqtrd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → 𝑝 ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
58		nelsn	⊢ ( 𝑝 ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → ¬ 𝑝 ∈ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
59	57 58	syl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → ¬ 𝑝 ∈ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
60		nelne1	⊢ ( ( 𝑝 ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∧ ¬ 𝑝 ∈ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
61	51 59 60	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ) ∧ 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ) → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
62	14 1 17 2 3	irngnzply1	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = ∪ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) )
63	5 62	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) )
64		eliun	⊢ ( 𝐴 ∈ ∪ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) ↔ ∃ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) )
65	63 64	sylib	⊢ ( 𝜑 → ∃ 𝑝 ∈ ( dom ( 𝐸 evalSub₁ 𝐹 ) ∖ { 𝑍 } ) 𝐴 ∈ ( ^◡ ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) “ { ( 0_g ‘ 𝐸 ) } ) )
66	61 65	r19.29a	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
67	33 66	eqnetrrd	⊢ ( 𝜑 → ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
68		eqid	⊢ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
69	22 68 32	pidlnzb	⊢ ( ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring ∧ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ) → ( ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ↔ ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) )
70	69	biimpar	⊢ ( ( ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring ∧ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ) ∧ ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
71	13 31 67 70	syl21anc	⊢ ( 𝜑 → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
72	14 11 15 2 3 19 17 20 32 28 4	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) )
73	71 72 55	3netr4d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )

Metamath Proof Explorer

Theorem irngnminplynz

Proof