Metamath Proof Explorer


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 < ( 𝐸 [:] 𝐹 ) )