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

Metamath Proof Explorer

Definition df-minply

Description: Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025)

Ref Expression
Assertion df-minply minPoly = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminply ⊢ minPoly
1 ve ⊢ 𝑒
2 cvv ⊢ V
3 vf ⊢ 𝑓
4 vx ⊢ 𝑥
5 cbs ⊢ Base
6 1 cv ⊢ 𝑒
7 6 5 cfv ⊢ ( Base ‘ 𝑒 )
8 cig1p ⊢ idlGen1p
9 cress ⊢ ↾s
10 3 cv ⊢ 𝑓
11 6 10 9 co ⊢ ( 𝑒 ↾s 𝑓 )
12 11 8 cfv ⊢ ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) )
13 vp ⊢ 𝑝
14 ces1 ⊢ evalSub1
15 6 10 14 co ⊢ ( 𝑒 evalSub1 𝑓 )
16 15 cdm ⊢ dom ( 𝑒 evalSub1 𝑓 )
17 13 cv ⊢ 𝑝
18 17 15 cfv ⊢ ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 )
19 4 cv ⊢ 𝑥
20 19 18 cfv ⊢ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 )
21 c0g ⊢ 0g
22 6 21 cfv ⊢ ( 0g ‘ 𝑒 )
23 20 22 wceq ⊢ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 )
24 23 13 16 crab ⊢ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) }
25 24 12 cfv ⊢ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } )
26 4 7 25 cmpt ⊢ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) )
27 1 3 2 2 26 cmpo ⊢ ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) )
28 0 27 wceq ⊢ minPoly = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑒 ) ↦ ( ( idlGen1p ‘ ( 𝑒 ↾s 𝑓 ) ) ‘ { 𝑝 ∈ dom ( 𝑒 evalSub1 𝑓 ) ∣ ( ( ( 𝑒 evalSub1 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) } ) ) )