Theorem minplyval 33668

Description: Expand the value of the minimal polynomial (𝑀‘𝐴) for a given element 𝐴. It is defined as the unique monic polynomial of minimal degree which annihilates 𝐴. By ply1annig1p 33667, that polynomial generates the ideal of the annihilators of 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.)

Hypotheses

Ref	Expression
ply1annig1p.o	⊢ 𝑂 = (𝐸 evalSub1 𝐹)
ply1annig1p.p	⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
ply1annig1p.b	⊢ 𝐵 = (Base‘𝐸)
ply1annig1p.e	⊢ (𝜑 → 𝐸 ∈ Field)
ply1annig1p.f	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
ply1annig1p.a	⊢ (𝜑 → 𝐴 ∈ 𝐵)
ply1annig1p.0	⊢ 0 = (0g‘𝐸)
ply1annig1p.q	⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }
ply1annig1p.k	⊢ 𝐾 = (RSpan‘𝑃)
ply1annig1p.g	⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))
minplyval.1	⊢ 𝑀 = (𝐸 minPoly 𝐹)

Assertion

Ref	Expression
minplyval	⊢ (𝜑 → (𝑀‘𝐴) = (𝐺‘𝑄))

Distinct variable groups:   0 ,𝑞   𝐴,𝑞   𝑂,𝑞   𝑃,𝑞   𝜑,𝑞   𝐸,𝑞   𝐹,𝑞

Allowed substitution hints:   𝐵(𝑞)   𝑄(𝑞)   𝐺(𝑞)   𝐾(𝑞)   𝑀(𝑞)

Proof of Theorem minplyval

Dummy variables 𝑒 𝑓 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		minplyval.1	. . 3 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
2		ply1annig1p.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
3	2	elexd 3468	. . . 4 ⊢ (𝜑 → 𝐸 ∈ V)
4		ply1annig1p.f	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
5	4	elexd 3468	. . . 4 ⊢ (𝜑 → 𝐹 ∈ V)
6		ply1annig1p.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐸)
7	6	fvexi 6854	. . . . . 6 ⊢ 𝐵 ∈ V
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
9	8	mptexd 7180	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })) ∈ V)
10		fveq2 6840	. . . . . . . 8 ⊢ (𝑒 = 𝐸 → (Base‘𝑒) = (Base‘𝐸))
11	10, 6	eqtr4di 2782	. . . . . . 7 ⊢ (𝑒 = 𝐸 → (Base‘𝑒) = 𝐵)
12	11	adantr 480	. . . . . 6 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (Base‘𝑒) = 𝐵)
13		oveq12 7378	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑒 ↾s 𝑓) = (𝐸 ↾s 𝐹))
14	13	fveq2d 6844	. . . . . . . 8 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (idlGen1p‘(𝑒 ↾s 𝑓)) = (idlGen1p‘(𝐸 ↾s 𝐹)))
15		ply1annig1p.g	. . . . . . . 8 ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))
16	14, 15	eqtr4di 2782	. . . . . . 7 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (idlGen1p‘(𝑒 ↾s 𝑓)) = 𝐺)
17		oveq12 7378	. . . . . . . . . 10 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = (𝐸 evalSub1 𝐹))
18		ply1annig1p.o	. . . . . . . . . 10 ⊢ 𝑂 = (𝐸 evalSub1 𝐹)
19	17, 18	eqtr4di 2782	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑒 evalSub1 𝑓) = 𝑂)
20	19	dmeqd 5859	. . . . . . . 8 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → dom (𝑒 evalSub1 𝑓) = dom 𝑂)
21	19	fveq1d 6842	. . . . . . . . . 10 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ((𝑒 evalSub1 𝑓)‘𝑞) = (𝑂‘𝑞))
22	21	fveq1d 6842	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = ((𝑂‘𝑞)‘𝑥))
23		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑒 = 𝐸 → (0g‘𝑒) = (0g‘𝐸))
24	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (0g‘𝑒) = (0g‘𝐸))
25		ply1annig1p.0	. . . . . . . . . 10 ⊢ 0 = (0g‘𝐸)
26	24, 25	eqtr4di 2782	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (0g‘𝑒) = 0 )
27	22, 26	eqeq12d 2745	. . . . . . . 8 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ((((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = (0g‘𝑒) ↔ ((𝑂‘𝑞)‘𝑥) = 0 ))
28	20, 27	rabeqbidv 3421	. . . . . . 7 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → {𝑞 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = (0g‘𝑒)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })
29	16, 28	fveq12d 6847	. . . . . 6 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑞 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = (0g‘𝑒)}) = (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 }))
30	12, 29	mpteq12dv 5189	. . . . 5 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑞 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = (0g‘𝑒)})) = (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })))
31		df-minply 33663	. . . . 5 ⊢ minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑞 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑞)‘𝑥) = (0g‘𝑒)})))
32	30, 31	ovmpoga 7523	. . . 4 ⊢ ((𝐸 ∈ V ∧ 𝐹 ∈ V ∧ (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })) ∈ V) → (𝐸 minPoly 𝐹) = (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })))
33	3, 5, 9, 32	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝐸 minPoly 𝐹) = (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })))
34	1, 33	eqtrid 2776	. 2 ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵 ↦ (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 })))
35		fveqeq2 6849	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝑂‘𝑞)‘𝑥) = 0 ↔ ((𝑂‘𝑞)‘𝐴) = 0 ))
36	35	rabbidv 3410	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 } = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 })
37		ply1annig1p.q	. . . . 5 ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }
38	36, 37	eqtr4di 2782	. . . 4 ⊢ (𝑥 = 𝐴 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 } = 𝑄)
39	38	fveq2d 6844	. . 3 ⊢ (𝑥 = 𝐴 → (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 }) = (𝐺‘𝑄))
40	39	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐺‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝑥) = 0 }) = (𝐺‘𝑄))
41		ply1annig1p.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
42		fvexd 6855	. 2 ⊢ (𝜑 → (𝐺‘𝑄) ∈ V)
43	34, 40, 41, 42	fvmptd 6957	1 ⊢ (𝜑 → (𝑀‘𝐴) = (𝐺‘𝑄))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3402  Vcvv 3444   ↦ cmpt 5183  dom cdm 5631  ‘cfv 6499  (class class class)co 7369  Basecbs 17155   ↾_s cress 17176  0_gc0g 17378  Fieldcfield 20615  SubDRingcsdrg 20671  RSpancrsp 21093  Poly₁cpl1 22037   evalSub₁ ces1 22176  idlGen_1pcig1p 26011   minPoly cminply 33662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-minply 33663

This theorem is referenced by:  minplycl  33669  minplymindeg  33671  minplyann  33672  minplyirredlem  33673  minplyirred  33674  irngnminplynz  33675  minplym1p  33676  minplynzm1p  33677  irredminply  33679  algextdeglem4  33683  algextdeglem5  33684