Definition df-algext

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

	Ref	Expression
Assertion	df-algext	$$⊢{/}_{\mathrm{AlgExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge \forall x\in {\mathrm{Base}}_e\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		calgext	$$class{/}_{\mathrm{AlgExt}}$$
1		ve	$$setvare$$
2		vf	$$setvarf$$
3	1	cv	$$setvare$$
4		cfldext	$$class{/}_{\mathrm{FldExt}}$$
5	2	cv	$$setvarf$$
6	3 5 4	wbr	$$wffe{/}_{\mathrm{FldExt}}f$$
7		vx	$$setvarx$$
8		cbs	$$class\mathrm{Base}$$
9	3 8	cfv	$$class{\mathrm{Base}}_e$$
10		vp	$$setvarp$$
11		cpl1	$$class{\mathrm{Poly}}_1$$
12	5 11	cfv	$$class{\mathrm{Poly}}_1\left(f\right)$$
13		ce1	$$class{\mathrm{eval}}_1$$
14	5 13	cfv	$$class{\mathrm{eval}}_1\left(f\right)$$
15	10	cv	$$setvarp$$
16	15 14	cfv	$$class{\mathrm{eval}}_1\left(f\right)\left(p\right)$$
17	7	cv	$$setvarx$$
18	17 16	cfv	$$class{\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)$$
19		c0g	$$class{0}_{𝑔}$$
20	3 19	cfv	$$class{0}_e$$
21	18 20	wceq	$$wff{\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e$$
22	21 10 12	wrex	$$wff\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e$$
23	22 7 9	wral	$$wff\forall x\in {\mathrm{Base}}_e\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e$$
24	6 23	wa	$$wff\left(e{/}_{\mathrm{FldExt}}f\wedge \forall x\in {\mathrm{Base}}_e\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e\right)$$
25	24 1 2	copab	$$class\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge \forall x\in {\mathrm{Base}}_e\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e\right)\right\}$$
26	0 25	wceq	$$wff{/}_{\mathrm{AlgExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge \forall x\in {\mathrm{Base}}_e\exists p\in {\mathrm{Poly}}_1\left(f\right){\mathrm{eval}}_1\left(f\right)\left(p\right)\left(x\right)=0_e\right)\right\}$$