Definition df-algext

Description: Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	df-algext	⊢ /AlgExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑒 ) ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		calgext	⊢ /AlgExt
1		ve	⊢ 𝑒
2		vf	⊢ 𝑓
3	1	cv	⊢ 𝑒
4		cfldext	⊢ /FldExt
5	2	cv	⊢ 𝑓
6	3 5 4	wbr	⊢ 𝑒 /FldExt 𝑓
7		vx	⊢ 𝑥
8		cbs	⊢ Base
9	3 8	cfv	⊢ ( Base ‘ 𝑒 )
10		vp	⊢ 𝑝
11		cpl1	⊢ Poly1
12	5 11	cfv	⊢ ( Poly1 ‘ 𝑓 )
13		ce1	⊢ eval1
14	5 13	cfv	⊢ ( eval1 ‘ 𝑓 )
15	10	cv	⊢ 𝑝
16	15 14	cfv	⊢ ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 )
17	7	cv	⊢ 𝑥
18	17 16	cfv	⊢ ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 )
19		c0g	⊢ 0g
20	3 19	cfv	⊢ ( 0g ‘ 𝑒 )
21	18 20	wceq	⊢ ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 )
22	21 10 12	wrex	⊢ ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 )
23	22 7 9	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑒 ) ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 )
24	6 23	wa	⊢ ( 𝑒 /FldExt 𝑓 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑒 ) ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) )
25	24 1 2	copab	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑒 ) ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) ) }
26	0 25	wceq	⊢ /AlgExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑒 ) ∃ 𝑝 ∈ ( Poly1 ‘ 𝑓 ) ( ( ( eval1 ‘ 𝑓 ) ‘ 𝑝 ) ‘ 𝑥 ) = ( 0g ‘ 𝑒 ) ) }