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