Theorem brfinext

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

	Ref	Expression
Assertion	brfinext	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
2		fldextfld2	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
3		breq12	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 /FldExt 𝑓 ↔ 𝐸 /FldExt 𝐹 ) )
4		oveq12	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 [:] 𝑓 ) = ( 𝐸 [:] 𝐹 ) )
5	4	eleq1d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
6	3 5	anbi12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
7		df-finext	⊢ /FinExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) }
8	6 7	brabga	⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
9	1 2 8	syl2anc	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) ) )
10	9	bianabs	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )