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

Metamath Proof Explorer

Theorem finextfldext

Description: A finite field extension is a field extension. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypothesis finextfldext.1 ⊢ φ → E /FinExt F
Assertion finextfldext ⊢ φ → E /FldExt F

Proof

Step Hyp Ref Expression
1 finextfldext.1 ⊢ φ → E /FinExt F
2 df-finext ⊢ /FinExt = e f | e /FldExt f ∧ e .:. f ∈ ℕ 0
3 2 relopabiv ⊢ Rel ⁡ /FinExt
4 3 brrelex1i ⊢ E /FinExt F → E ∈ V
5 1 4 syl ⊢ φ → E ∈ V
6 3 brrelex2i ⊢ E /FinExt F → F ∈ V
7 1 6 syl ⊢ φ → F ∈ V
8 breq12 ⊢ e = E ∧ f = F → e /FldExt f ↔ E /FldExt F
9 oveq12 ⊢ e = E ∧ f = F → e .:. f = E .:. F
10 9 eleq1d ⊢ e = E ∧ f = F → e .:. f ∈ ℕ 0 ↔ E .:. F ∈ ℕ 0
11 8 10 anbi12d ⊢ e = E ∧ f = F → e /FldExt f ∧ e .:. f ∈ ℕ 0 ↔ E /FldExt F ∧ E .:. F ∈ ℕ 0
12 11 2 brabga ⊢ E ∈ V ∧ F ∈ V → E /FinExt F ↔ E /FldExt F ∧ E .:. F ∈ ℕ 0
13 5 7 12 syl2anc ⊢ φ → E /FinExt F ↔ E /FldExt F ∧ E .:. F ∈ ℕ 0
14 1 13 mpbid ⊢ φ → E /FldExt F ∧ E .:. F ∈ ℕ 0
15 14 simpld ⊢ φ → E /FldExt F