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 ‘ 𝑒 ) } ) ) )