Metamath Proof Explorer

Theorem bralgext

Description: Express the fact that a field extension E / F is algebraic. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses bralgext.b ⊢ B = Base E
bralgext.c ⊢ C = Base F
bralgext.e ⊢ φ → E ∈ V
bralgext.f ⊢ φ → F ∈ V
Assertion bralgext ⊢ φ → E /AlgExt F ↔ E /FldExt F ∧ E IntgRing C = B

Proof

Step Hyp Ref Expression
1 bralgext.b ⊢ B = Base E
2 bralgext.c ⊢ C = Base F
3 bralgext.e ⊢ φ → E ∈ V
4 bralgext.f ⊢ φ → F ∈ V
5 breq12 ⊢ e = E ∧ f = F → e /FldExt f ↔ E /FldExt F
6 simpl ⊢ e = E ∧ f = F → e = E
7 fveq2 ⊢ f = F → Base f = Base F
8 7 2 eqtr4di ⊢ f = F → Base f = C
9 8 adantl ⊢ e = E ∧ f = F → Base f = C
10 6 9 oveq12d ⊢ e = E ∧ f = F → e IntgRing Base f = E IntgRing C
11 fveq2 ⊢ e = E → Base e = Base E
12 11 1 eqtr4di ⊢ e = E → Base e = B
13 12 adantr ⊢ e = E ∧ f = F → Base e = B
14 10 13 eqeq12d ⊢ e = E ∧ f = F → e IntgRing Base f = Base e ↔ E IntgRing C = B
15 5 14 anbi12d ⊢ e = E ∧ f = F → e /FldExt f ∧ e IntgRing Base f = Base e ↔ E /FldExt F ∧ E IntgRing C = B
16 df-algext ⊢ /AlgExt = e f | e /FldExt f ∧ e IntgRing Base f = Base e
17 15 16 brabga ⊢ E ∈ V ∧ F ∈ V → E /AlgExt F ↔ E /FldExt F ∧ E IntgRing C = B
18 3 4 17 syl2anc ⊢ φ → E /AlgExt F ↔ E /FldExt F ∧ E IntgRing C = B