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