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		isfld	$$⊢E\in \mathrm{Field}\leftrightarrow \left(E\in \mathrm{DivRing}\wedge E\in \mathrm{CRing}\right)$$
5	4	simplbi	$$⊢E\in \mathrm{Field}\to E\in \mathrm{DivRing}$$
6		rlmval	$$⊢\mathrm{ringLMod}\left(E\right)=\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)$$
7	6	eqcomi	$$⊢\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)=\mathrm{ringLMod}\left(E\right)$$
8	7	rlmdim	$$⊢E\in \mathrm{DivRing}\to \dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)\right)=1$$
9	5 8	syl	$$⊢E\in \mathrm{Field}\to \dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_E\right)\right)=1$$
10	3 9	eqtrd	$$⊢E\in \mathrm{Field}\to E\left[.:.\right]E=1$$