Metamath Proof Explorer

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 𝐾 ) ) )