brfinext

Description: The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023)

		Ref	Expression
	Assertion	brfinext	$⊢ E /_{FldExt} F \to (E /_{FinExt} F \leftrightarrow E [. : .] F \in ℕ_{0})$

Step	Hyp	Ref	Expression
1		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
2		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
3		breq12	$⊢ (e = E \land f = F) \to (e /_{FldExt} f \leftrightarrow E /_{FldExt} F)$
4		oveq12	$⊢ (e = E \land f = F) \to e [. : .] f = E [. : .] F$
5	4	eleq1d	$⊢ (e = E \land f = F) \to (e [. : .] f \in ℕ_{0} \leftrightarrow E [. : .] F \in ℕ_{0})$
6	3 5	anbi12d	$⊢ (e = E \land f = F) \to ((e /_{FldExt} f \land e [. : .] f \in ℕ_{0}) \leftrightarrow (E /_{FldExt} F \land E [. : .] F \in ℕ_{0}))$
7		df-finext	$⊢ /_{FinExt} = \{⟨e, f⟩ \| (e /_{FldExt} f \land e [. : .] f \in ℕ_{0})\}$
8	6 7	brabga	$⊢ (E \in Field \land F \in Field) \to (E /_{FinExt} F \leftrightarrow (E /_{FldExt} F \land E [. : .] F \in ℕ_{0}))$
9	1 2 8	syl2anc	$⊢ E /_{FldExt} F \to (E /_{FinExt} F \leftrightarrow (E /_{FldExt} F \land E [. : .] F \in ℕ_{0}))$
10	9	bianabs	$⊢ E /_{FldExt} F \to (E /_{FinExt} F \leftrightarrow E [. : .] F \in ℕ_{0})$

Metamath Proof Explorer