Theorem extdgid

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

	Ref	Expression
Assertion	extdgid	$$⊢E\in \mathrm{Field}\to E\left[.:.\right]E=1$$

Proof

Step	Hyp	Ref	Expression
1		fldextid	$$⊢E\in \mathrm{Field}\to E{/}_{\mathrm{FldExt}}E$$
2		extdgval	$$⊢E{/}_{\mathrm{FldExt}}E\to E\left[.:.\right]E=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)\right)$$
3	1 2	syl	$$⊢E\in \mathrm{Field}\to E\left[.:.\right]E=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)\right)$$
4		rlmval	$$⊢\mathrm{ringLMod}\left(E\right)=\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)$$
5	4	eqcomi	$$⊢\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)=\mathrm{ringLMod}\left(E\right)$$
6	5	rgmoddim	$$⊢E\in \mathrm{Field}\to \dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)\right)=1$$
7	3 6	eqtrd	$$⊢E\in \mathrm{Field}\to E\left[.:.\right]E=1$$