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	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FinExt 𝐾 ↔ ( 𝐸 /FinExt 𝐹 ∧ 𝐹 /FinExt 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		extdgmul	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) )
2	1	eleq1d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( 𝐸 [:] 𝐾 ) ∈ ℕ0 ↔ ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) ∈ ℕ0 ) )
3		fldexttr	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐾 )
4		brfinext	⊢ ( 𝐸 /FldExt 𝐾 → ( 𝐸 /FinExt 𝐾 ↔ ( 𝐸 [:] 𝐾 ) ∈ ℕ0 ) )
5	3 4	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FinExt 𝐾 ↔ ( 𝐸 [:] 𝐾 ) ∈ ℕ0 ) )
6		brfinext	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 /FinExt 𝐹 ↔ ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ) )
7		brfinext	⊢ ( 𝐹 /FldExt 𝐾 → ( 𝐹 /FinExt 𝐾 ↔ ( 𝐹 [:] 𝐾 ) ∈ ℕ0 ) )
8	6 7	bi2anan9	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( 𝐸 /FinExt 𝐹 ∧ 𝐹 /FinExt 𝐾 ) ↔ ( ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 [:] 𝐾 ) ∈ ℕ0 ) ) )
9		extdgcl	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) ∈ ℕ0* )
10	9	adantr	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐹 ) ∈ ℕ0* )
11		extdgcl	⊢ ( 𝐹 /FldExt 𝐾 → ( 𝐹 [:] 𝐾 ) ∈ ℕ0* )
12	11	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 [:] 𝐾 ) ∈ ℕ0* )
13		extdggt0	⊢ ( 𝐸 /FldExt 𝐹 → 0 < ( 𝐸 [:] 𝐹 ) )
14	13	adantr	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 0 < ( 𝐸 [:] 𝐹 ) )
15	14	gt0ne0d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐹 ) ≠ 0 )
16		extdggt0	⊢ ( 𝐹 /FldExt 𝐾 → 0 < ( 𝐹 [:] 𝐾 ) )
17	16	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 0 < ( 𝐹 [:] 𝐾 ) )
18	17	gt0ne0d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 [:] 𝐾 ) ≠ 0 )
19		nn0xmulclb	⊢ ( ( ( ( 𝐸 [:] 𝐹 ) ∈ ℕ0* ∧ ( 𝐹 [:] 𝐾 ) ∈ ℕ0* ) ∧ ( ( 𝐸 [:] 𝐹 ) ≠ 0 ∧ ( 𝐹 [:] 𝐾 ) ≠ 0 ) ) → ( ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) ∈ ℕ0 ↔ ( ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 [:] 𝐾 ) ∈ ℕ0 ) ) )
20	10 12 15 18 19	syl22anc	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) ∈ ℕ0 ↔ ( ( 𝐸 [:] 𝐹 ) ∈ ℕ0 ∧ ( 𝐹 [:] 𝐾 ) ∈ ℕ0 ) ) )
21	8 20	bitr4d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( 𝐸 /FinExt 𝐹 ∧ 𝐹 /FinExt 𝐾 ) ↔ ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) ∈ ℕ0 ) )
22	2 5 21	3bitr4d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FinExt 𝐾 ↔ ( 𝐸 /FinExt 𝐹 ∧ 𝐹 /FinExt 𝐾 ) ) )