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

Metamath Proof Explorer

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