Theorem fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	fldextid	$$⊢F\in \mathrm{Field}\to F{/}_{\mathrm{FldExt}}F$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
2	1	ressid	$$⊢F\in \mathrm{Field}\to F{\upharpoonright }_{𝑠}{\mathrm{Base}}_F=F$$
3	2	eqcomd	$$⊢F\in \mathrm{Field}\to F=F{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
4		isfld	$$⊢F\in \mathrm{Field}\leftrightarrow \left(F\in \mathrm{DivRing}\wedge F\in \mathrm{CRing}\right)$$
5	4	simplbi	$$⊢F\in \mathrm{Field}\to F\in \mathrm{DivRing}$$
6		drngring	$$⊢F\in \mathrm{DivRing}\to F\in \mathrm{Ring}$$
7	1	subrgid	$$⊢F\in \mathrm{Ring}\to {\mathrm{Base}}_F\in \mathrm{SubRing}\left(F\right)$$
8	5 6 7	3syl	$$⊢F\in \mathrm{Field}\to {\mathrm{Base}}_F\in \mathrm{SubRing}\left(F\right)$$
9		brfldext	$$⊢\left(F\in \mathrm{Field}\wedge F\in \mathrm{Field}\right)\to \left(F{/}_{\mathrm{FldExt}}F\leftrightarrow \left(F=F{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\wedge {\mathrm{Base}}_F\in \mathrm{SubRing}\left(F\right)\right)\right)$$
10	9	anidms	$$⊢F\in \mathrm{Field}\to \left(F{/}_{\mathrm{FldExt}}F\leftrightarrow \left(F=F{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\wedge {\mathrm{Base}}_F\in \mathrm{SubRing}\left(F\right)\right)\right)$$
11	3 8 10	mpbir2and	$$⊢F\in \mathrm{Field}\to F{/}_{\mathrm{FldExt}}F$$