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 ⊢ ( 𝜑 → 𝐸 /FinExt 𝐹 )
Assertion finextfldext ( 𝜑 → 𝐸 /FldExt 𝐹 )

Proof

Step Hyp Ref Expression
1 finextfldext.1 ⊢ ( 𝜑 → 𝐸 /FinExt 𝐹 )
2 df-finext ⊢ /FinExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) }
3 2 relopabiv ⊢ Rel /FinExt
4 3 brrelex1i ⊢ ( 𝐸 /FinExt 𝐹 → 𝐸 ∈ V )
5 1 4 syl ⊢ ( 𝜑 → 𝐸 ∈ V )
6 3 brrelex2i ⊢ ( 𝐸 /FinExt 𝐹 → 𝐹 ∈ V )
7 1 6 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
8 breq12 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 /FldExt 𝑓 ↔ 𝐸 /FldExt 𝐹 ) )
9 oveq12 ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 [:] 𝑓 ) = ( 𝐸 [:] 𝐹 ) )
10 9 eleq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
11 8 10 anbi12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
12 11 2 brabga ⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
13 5 7 12 syl2anc ⊢ ( 𝜑 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
14 1 13 mpbid ⊢ ( 𝜑 → ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
15 14 simpld ⊢ ( 𝜑 → 𝐸 /FldExt 𝐹 )