This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldextfld2

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

Ref Expression
Assertion fldextfld2 ( 𝐸 /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 opelxp2 ⊢ ( ⟨ 𝐸 , 𝐹 ⟩ ∈ ( Field × Field ) → 𝐹 ∈ Field )
8 6 7 syl ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )