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 𝐹 )