Definition df-algext 31720

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

Assertion

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

Distinct variable group:   𝑒,𝑓,𝑝,𝑥

Detailed syntax breakdown of Definition df-algext

Step	Hyp	Ref	Expression
1		calgext 31715	. 2 class /AlgExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1538	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1538	. . . . 5 class 𝑓
6		cfldext 31713	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5074	. . . 4 wff 𝑒/FldExt𝑓
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1538	. . . . . . . 8 class 𝑥
10		vp	. . . . . . . . . 10 setvar 𝑝
11	10	cv 1538	. . . . . . . . 9 class 𝑝
12		ce1 21480	. . . . . . . . . 10 class eval1
13	5, 12	cfv 6433	. . . . . . . . 9 class (eval1‘𝑓)
14	11, 13	cfv 6433	. . . . . . . 8 class ((eval1‘𝑓)‘𝑝)
15	9, 14	cfv 6433	. . . . . . 7 class (((eval1‘𝑓)‘𝑝)‘𝑥)
16		c0g 17150	. . . . . . . 8 class 0g
17	3, 16	cfv 6433	. . . . . . 7 class (0g‘𝑒)
18	15, 17	wceq 1539	. . . . . 6 wff (((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)
19		cpl1 21348	. . . . . . 7 class Poly1
20	5, 19	cfv 6433	. . . . . 6 class (Poly1‘𝑓)
21	18, 10, 20	wrex 3065	. . . . 5 wff ∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)
22		cbs 16912	. . . . . 6 class Base
23	3, 22	cfv 6433	. . . . 5 class (Base‘𝑒)
24	21, 8, 23	wral 3064	. . . 4 wff ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)
25	7, 24	wa 396	. . 3 wff (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))
26	25, 2, 4	copab 5136	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))}
27	1, 26	wceq 1539	1 wff /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))}

This definition is referenced by: (None)