Definition df-fldext

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

	Ref	Expression
Assertion	df-fldext	⊢ /FldExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfldext	⊢ /FldExt
1		ve	⊢ 𝑒
2		vf	⊢ 𝑓
3	1	cv	⊢ 𝑒
4		cfield	⊢ Field
5	3 4	wcel	⊢ 𝑒 ∈ Field
6	2	cv	⊢ 𝑓
7	6 4	wcel	⊢ 𝑓 ∈ Field
8	5 7	wa	⊢ ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field )
9		cress	⊢ ↾s
10		cbs	⊢ Base
11	6 10	cfv	⊢ ( Base ‘ 𝑓 )
12	3 11 9	co	⊢ ( 𝑒 ↾s ( Base ‘ 𝑓 ) )
13	6 12	wceq	⊢ 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) )
14		csubrg	⊢ SubRing
15	3 14	cfv	⊢ ( SubRing ‘ 𝑒 )
16	11 15	wcel	⊢ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 )
17	13 16	wa	⊢ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) )
18	8 17	wa	⊢ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) )
19	18 1 2	copab	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) }
20	0 19	wceq	⊢ /FldExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) }