Theorem extdggt0

Description: Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	extdggt0	⊢ ( 𝐸 /FldExt 𝐹 → 0 < ( 𝐸 [:] 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
2		isfld	⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
3	2	simplbi	⊢ ( 𝐸 ∈ Field → 𝐸 ∈ DivRing )
4	1 3	syl	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ DivRing )
5		fldextress	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
6		fldextfld2	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
7		isfld	⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
8	7	simplbi	⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
9	6 8	syl	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ DivRing )
10	5 9	eqeltrrd	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing )
11		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
12	11	fldextsubrg	⊢ ( 𝐸 /FldExt 𝐹 → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
13		eqid	⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) )
14		eqid	⊢ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) )
15	13 14	sralvec	⊢ ( ( 𝐸 ∈ DivRing ∧ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
16	4 10 12 15	syl3anc	⊢ ( 𝐸 /FldExt 𝐹 → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec )
17		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
18	17	subrgss	⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
19	12 18	syl	⊢ ( 𝐸 /FldExt 𝐹 → ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
20	13 17	sradrng	⊢ ( ( 𝐸 ∈ DivRing ∧ ( Base ‘ 𝐹 ) ⊆ ( Base ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ DivRing )
21	4 19 20	syl2anc	⊢ ( 𝐸 /FldExt 𝐹 → ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ DivRing )
22		drngdimgt0	⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ LVec ∧ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ∈ DivRing ) → 0 < ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
23	16 21 22	syl2anc	⊢ ( 𝐸 /FldExt 𝐹 → 0 < ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
24		extdgval	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
25	23 24	breqtrrd	⊢ ( 𝐸 /FldExt 𝐹 → 0 < ( 𝐸 [:] 𝐹 ) )