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 )