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

Metamath Proof Explorer

Theorem minplyval

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

Ref Expression
Hypotheses 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 minplyval ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
2 ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
3 ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
5 ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6 ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 ply1annig1p.0 ⊢ 0 = ( 0g ‘ 𝐸 )
8 ply1annig1p.q ⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9 ply1annig1p.k ⊢ 𝐾 = ( RSpan ‘ 𝑃 )
10 ply1annig1p.g ⊢ 𝐺 = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
11 minplyval.1 ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
12 4 elexd ⊢ ( 𝜑 → 𝐸 ∈ V )
13 5 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
14 3 fvexi ⊢ 𝐵 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
16 15 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) ∈ V )
17 fveq2 ⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = ( Base ‘ 𝐸 ) )
18 17 3 eqtr4di ⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = 𝐵 )
19 18 adantr ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑒 ) = 𝐵 )
20 oveq12 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ↾s 𝑓 ) = ( 𝐸 ↾s 𝐹 ) )
21 20 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) )
22 21 10 eqtr4di ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) = 𝐺 )
23 oveq12 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 evalSub1 𝑓 ) = ( 𝐸 evalSub1 𝐹 ) )
24 23 1 eqtr4di ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 evalSub1 𝑓 ) = 𝑂 )
25 24 dmeqd ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → dom ( 𝑒 evalSub1 𝑓 ) = dom 𝑂 )
26 24 fveq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) = ( 𝑂 ‘ 𝑞 ) )
27 26 fveq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) )
28 fveq2 ⊢ ( 𝑒 = 𝐸 → ( 0g ‘ 𝑒 ) = ( 0g ‘ 𝐸 ) )
29 28 adantr ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑒 ) = ( 0g ‘ 𝐸 ) )
30 29 7 eqtr4di ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑒 ) = 0 )
31 27 30 eqeq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) ↔ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 ) )
32 25 31 rabeqbidv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } )
33 22 32 fveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) = ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) )
34 19 33 mpteq12dv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
35 df-minply ⊢ minPoly = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑞 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑞 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) )
36 34 35 ovmpoga ⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ V ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) ∈ V ) → ( 𝐸 minPoly 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
37 12 13 16 36 syl3anc ⊢ ( 𝜑 → ( 𝐸 minPoly 𝐹 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
38 11 37 eqtrid ⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) ) )
39 fveqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ) )
40 39 rabbidv ⊢ ( 𝑥 = 𝐴 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
41 40 8 eqtr4di ⊢ ( 𝑥 = 𝐴 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } = 𝑄 )
42 41 fveq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) = ( 𝐺 ‘ 𝑄 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐺 ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑥 ) = 0 } ) = ( 𝐺 ‘ 𝑄 ) )
44 fvexd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑄 ) ∈ V )
45 38 43 6 44 fvmptd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑄 ) )