Definition df-algext

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

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

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		cirng	⊢ IntgRing
8	3 5 7	co	⊢ ( 𝑒 IntgRing 𝑓 )
9		cbs	⊢ Base
10	3 9	cfv	⊢ ( Base ‘ 𝑒 )
11	8 10	wceq	⊢ ( 𝑒 IntgRing 𝑓 ) = ( Base ‘ 𝑒 )
12	6 11	wa	⊢ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 IntgRing 𝑓 ) = ( Base ‘ 𝑒 ) )
13	12 1 2	copab	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 IntgRing 𝑓 ) = ( Base ‘ 𝑒 ) ) }
14	0 13	wceq	⊢ /AlgExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 IntgRing 𝑓 ) = ( Base ‘ 𝑒 ) ) }