Definition df-algext 33688

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

Assertion

Ref	Expression
df-algext	⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing 𝑓) = (Base‘𝑒))}

Distinct variable group:   𝑒,𝑓

Detailed syntax breakdown of Definition df-algext

Step	Hyp	Ref	Expression
1		calgext 33687	. 2 class /AlgExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1539	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1539	. . . . 5 class 𝑓
6		cfldext 33634	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5107	. . . 4 wff 𝑒/FldExt𝑓
8		cirng 33678	. . . . . 6 class IntgRing
9	3, 5, 8	co 7387	. . . . 5 class (𝑒 IntgRing 𝑓)
10		cbs 17179	. . . . . 6 class Base
11	3, 10	cfv 6511	. . . . 5 class (Base‘𝑒)
12	9, 11	wceq 1540	. . . 4 wff (𝑒 IntgRing 𝑓) = (Base‘𝑒)
13	7, 12	wa 395	. . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing 𝑓) = (Base‘𝑒))
14	13, 2, 4	copab 5169	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing 𝑓) = (Base‘𝑒))}
15	1, 14	wceq 1540	1 wff /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing 𝑓) = (Base‘𝑒))}

This definition is referenced by: (None)