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

Metamath Proof Explorer

Theorem extdgid

Description: A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023)

Ref Expression
Assertion extdgid ( 𝐸 ∈ Field → ( 𝐸 [:] 𝐸 ) = 1 )

Proof

Step Hyp Ref Expression
1 fldextid ⊢ ( 𝐸 ∈ Field → 𝐸 /FldExt 𝐸 )
2 extdgval ⊢ ( 𝐸 /FldExt 𝐸 → ( 𝐸 [:] 𝐸 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) ) )
3 1 2 syl ⊢ ( 𝐸 ∈ Field → ( 𝐸 [:] 𝐸 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) ) )
4 isfld ⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
5 4 simplbi ⊢ ( 𝐸 ∈ Field → 𝐸 ∈ DivRing )
6 rlmval ⊢ ( ringLMod ‘ 𝐸 ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) )
7 6 eqcomi ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) = ( ringLMod ‘ 𝐸 )
8 7 rlmdim ⊢ ( 𝐸 ∈ DivRing → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) ) = 1 )
9 5 8 syl ⊢ ( 𝐸 ∈ Field → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) ) = 1 )
10 3 9 eqtrd ⊢ ( 𝐸 ∈ Field → ( 𝐸 [:] 𝐸 ) = 1 )