Theorem fldextfld1

Description: A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )

Proof

Step	Hyp	Ref	Expression
1		opabssxp	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) } ⊆ ( Field × Field )
2		df-br	⊢ ( 𝐸 /FldExt 𝐹 ↔ ⟨ 𝐸 , 𝐹 ⟩ ∈ /FldExt )
3	2	biimpi	⊢ ( 𝐸 /FldExt 𝐹 → ⟨ 𝐸 , 𝐹 ⟩ ∈ /FldExt )
4		df-fldext	⊢ /FldExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) }
5	3 4	eleqtrdi	⊢ ( 𝐸 /FldExt 𝐹 → ⟨ 𝐸 , 𝐹 ⟩ ∈ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( ( 𝑒 ∈ Field ∧ 𝑓 ∈ Field ) ∧ ( 𝑓 = ( 𝑒 ↾s ( Base ‘ 𝑓 ) ) ∧ ( Base ‘ 𝑓 ) ∈ ( SubRing ‘ 𝑒 ) ) ) } )
6	1 5	sselid	⊢ ( 𝐸 /FldExt 𝐹 → ⟨ 𝐸 , 𝐹 ⟩ ∈ ( Field × Field ) )
7		opelxp1	⊢ ( ⟨ 𝐸 , 𝐹 ⟩ ∈ ( Field × Field ) → 𝐸 ∈ Field )
8	6 7	syl	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )