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		rlmval	⊢ ( ringLMod ‘ 𝐸 ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) )
5	4	eqcomi	⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) = ( ringLMod ‘ 𝐸 )
6	5	rgmoddim	⊢ ( 𝐸 ∈ Field → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐸 ) ) ) = 1 )
7	3 6	eqtrd	⊢ ( 𝐸 ∈ Field → ( 𝐸 [:] 𝐸 ) = 1 )