This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem extdgcl

Description: Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion extdgcl ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) ∈ ℕ0* )

Proof

Step Hyp Ref Expression
1 extdgval ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
2 fldextfld1 ⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
3 isfld ⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
4 2 3 sylib ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
5 4 simpld ⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ DivRing )
6 fldextress ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
7 fldextfld2 ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
8 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
9 7 8 sylib ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
10 9 simpld ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ DivRing )
11 6 10 eqeltrrd ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing )
12 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
13 12 fldextsubrg ⊢ ( 𝐸 /FldExt 𝐹 → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
14 eqid ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) )
15 eqid ⊢ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) )
16 14 15 sralvec ⊢ ( ( 𝐸 ∈ DivRing ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
17 5 11 13 16 syl3anc ⊢ ( 𝐸 /FldExt 𝐹 → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
18 dimcl ⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ ℕ0* )
19 17 18 syl ⊢ ( 𝐸 /FldExt 𝐹 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ ℕ0* )
20 1 19 eqeltrd ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) ∈ ℕ0* )