Theorem extdgval

Description: Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	extdgval	$$⊢E{/}_{\mathrm{FldExt}}F\to E\left[.:.\right]F=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		relfldext	$$⊢\mathrm{Rel}{/}_{\mathrm{FldExt}}$$
2	1	brrelex1i	$$⊢E{/}_{\mathrm{FldExt}}F\to E\in \mathrm{V}$$
3		elrelimasn	$$⊢\mathrm{Rel}{/}_{\mathrm{FldExt}}\to \left(F\in {/}_{\mathrm{FldExt}}\left[\left\{E\right\}\right]\leftrightarrow E{/}_{\mathrm{FldExt}}F\right)$$
4	1 3	ax-mp	$$⊢F\in {/}_{\mathrm{FldExt}}\left[\left\{E\right\}\right]\leftrightarrow E{/}_{\mathrm{FldExt}}F$$
5	4	biimpri	$$⊢E{/}_{\mathrm{FldExt}}F\to F\in {/}_{\mathrm{FldExt}}\left[\left\{E\right\}\right]$$
6		fvexd	$$⊢E{/}_{\mathrm{FldExt}}F\to \dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)\in \mathrm{V}$$
7		simpl	$$⊢\left(e=E\wedge f=F\right)\to e=E$$
8	7	fveq2d	$$⊢\left(e=E\wedge f=F\right)\to \mathrm{subringAlg}\left(e\right)=\mathrm{subringAlg}\left(E\right)$$
9		simpr	$$⊢\left(e=E\wedge f=F\right)\to f=F$$
10	9	fveq2d	$$⊢\left(e=E\wedge f=F\right)\to {\mathrm{Base}}_f={\mathrm{Base}}_F$$
11	8 10	fveq12d	$$⊢\left(e=E\wedge f=F\right)\to \mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)=\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)$$
12	11	fveq2d	$$⊢\left(e=E\wedge f=F\right)\to \dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)$$
13		sneq	$$⊢e=E\to \left\{e\right\}=\left\{E\right\}$$
14	13	imaeq2d	$$⊢e=E\to {/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]={/}_{\mathrm{FldExt}}\left[\left\{E\right\}\right]$$
15		df-extdg	$$⊢\left[.:.\right]=\left(e\in \mathrm{V},f\in {/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]⟼\dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)\right)$$
16	12 14 15	ovmpox	$$⊢\left(E\in \mathrm{V}\wedge F\in {/}_{\mathrm{FldExt}}\left[\left\{E\right\}\right]\wedge \dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)\in \mathrm{V}\right)\to E\left[.:.\right]F=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)$$
17	2 5 6 16	syl3anc	$$⊢E{/}_{\mathrm{FldExt}}F\to E\left[.:.\right]F=\dim \left(\mathrm{subringAlg}\left(E\right)\left({\mathrm{Base}}_F\right)\right)$$