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	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (E /_{FinExt} K \leftrightarrow (E /_{FinExt} F \land F /_{FinExt} K))$

Proof

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

Metamath Proof Explorer

Theorem finexttrb

Proof