Theorem finexttrb

Description: The extension E of K is finite if and only if E is finite over F and F is finite over K . Corollary 1.3 of Lang , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	finexttrb	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to \left(E{/}_{\mathrm{FinExt}}K\leftrightarrow \left(E{/}_{\mathrm{FinExt}}F\wedge F{/}_{\mathrm{FinExt}}K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		extdgmul
2	1	eleq1d
3		fldexttr	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to E{/}_{\mathrm{FldExt}}K$$
4		brfinext	$$⊢E{/}_{\mathrm{FldExt}}K\to \left(E{/}_{\mathrm{FinExt}}K\leftrightarrow E\left[.:.\right]K\in {\mathbb{N}}_0\right)$$
5	3 4	syl	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to \left(E{/}_{\mathrm{FinExt}}K\leftrightarrow E\left[.:.\right]K\in {\mathbb{N}}_0\right)$$
6		brfinext	$$⊢E{/}_{\mathrm{FldExt}}F\to \left(E{/}_{\mathrm{FinExt}}F\leftrightarrow E\left[.:.\right]F\in {\mathbb{N}}_0\right)$$
7		brfinext	$$⊢F{/}_{\mathrm{FldExt}}K\to \left(F{/}_{\mathrm{FinExt}}K\leftrightarrow F\left[.:.\right]K\in {\mathbb{N}}_0\right)$$
8	6 7	bi2anan9	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to \left(\left(E{/}_{\mathrm{FinExt}}F\wedge F{/}_{\mathrm{FinExt}}K\right)\leftrightarrow \left(E\left[.:.\right]F\in {\mathbb{N}}_0\wedge F\left[.:.\right]K\in {\mathbb{N}}_0\right)\right)$$
9		extdgcl	$$⊢E{/}_{\mathrm{FldExt}}F\to E\left[.:.\right]F\in {\mathbb{N}}_0^{*}$$
10	9	adantr	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to E\left[.:.\right]F\in {\mathbb{N}}_0^{*}$$
11		extdgcl	$$⊢F{/}_{\mathrm{FldExt}}K\to F\left[.:.\right]K\in {\mathbb{N}}_0^{*}$$
12	11	adantl	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to F\left[.:.\right]K\in {\mathbb{N}}_0^{*}$$
13		extdggt0	$$⊢E{/}_{\mathrm{FldExt}}F\to 0<E\left[.:.\right]F$$
14	13	adantr	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to 0<E\left[.:.\right]F$$
15	14	gt0ne0d	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to E\left[.:.\right]F\ne 0$$
16		extdggt0	$$⊢F{/}_{\mathrm{FldExt}}K\to 0<F\left[.:.\right]K$$
17	16	adantl	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to 0<F\left[.:.\right]K$$
18	17	gt0ne0d	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to F\left[.:.\right]K\ne 0$$
19		nn0xmulclb
20	10 12 15 18 19	syl22anc
21	8 20	bitr4d
22	2 5 21	3bitr4d	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge F{/}_{\mathrm{FldExt}}K\right)\to \left(E{/}_{\mathrm{FinExt}}K\leftrightarrow \left(E{/}_{\mathrm{FinExt}}F\wedge F{/}_{\mathrm{FinExt}}K\right)\right)$$