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	⊢ 𝐵 = ( Base ‘ 𝐸 )
	bralgext.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
	bralgext.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	bralgext.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	bralgext	⊢ ( 𝜑 → ( 𝐸 /AlgExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 IntgRing 𝐶 ) = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bralgext.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
2		bralgext.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
3		bralgext.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
4		bralgext.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5		breq12	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 /FldExt 𝑓 ↔ 𝐸 /FldExt 𝐹 ) )
6		simpl	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑒 = 𝐸 )
7		fveq2	⊢ ( 𝑓 = 𝐹 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
8	7 2	eqtr4di	⊢ ( 𝑓 = 𝐹 → ( Base ‘ 𝑓 ) = 𝐶 )
9	8	adantl	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐶 )
10	6 9	oveq12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 IntgRing ( Base ‘ 𝑓 ) ) = ( 𝐸 IntgRing 𝐶 ) )
11		fveq2	⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = ( Base ‘ 𝐸 ) )
12	11 1	eqtr4di	⊢ ( 𝑒 = 𝐸 → ( Base ‘ 𝑒 ) = 𝐵 )
13	12	adantr	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑒 ) = 𝐵 )
14	10 13	eqeq12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 IntgRing ( Base ‘ 𝑓 ) ) = ( Base ‘ 𝑒 ) ↔ ( 𝐸 IntgRing 𝐶 ) = 𝐵 ) )
15	5 14	anbi12d	⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 IntgRing ( Base ‘ 𝑓 ) ) = ( Base ‘ 𝑒 ) ) ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 IntgRing 𝐶 ) = 𝐵 ) ) )
16		df-algext	⊢ /AlgExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 IntgRing ( Base ‘ 𝑓 ) ) = ( Base ‘ 𝑒 ) ) }
17	15 16	brabga	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) → ( 𝐸 /AlgExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 IntgRing 𝐶 ) = 𝐵 ) ) )
18	3 4 17	syl2anc	⊢ ( 𝜑 → ( 𝐸 /AlgExt 𝐹 ↔ ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 IntgRing 𝐶 ) = 𝐵 ) ) )