Theorem extdg1b

Description: The degree of the extension E /FldExt F is 1 iff E and F are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023)

	Ref	Expression
Assertion	extdg1b	$$⊢E{/}_{\mathrm{FldExt}}F\to \left(E\left[.:.\right]F=1\leftrightarrow E=F\right)$$

Proof

Step	Hyp	Ref	Expression
1		extdg1id	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge E\left[.:.\right]F=1\right)\to E=F$$
2		oveq1	$$⊢E=F\to E\left[.:.\right]F=F\left[.:.\right]F$$
3	2	adantl	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge E=F\right)\to E\left[.:.\right]F=F\left[.:.\right]F$$
4		fldextfld2	$$⊢E{/}_{\mathrm{FldExt}}F\to F\in \mathrm{Field}$$
5	4	adantr	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge E=F\right)\to F\in \mathrm{Field}$$
6		extdgid	$$⊢F\in \mathrm{Field}\to F\left[.:.\right]F=1$$
7	5 6	syl	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge E=F\right)\to F\left[.:.\right]F=1$$
8	3 7	eqtrd	$$⊢\left(E{/}_{\mathrm{FldExt}}F\wedge E=F\right)\to E\left[.:.\right]F=1$$
9	1 8	impbida	$$⊢E{/}_{\mathrm{FldExt}}F\to \left(E\left[.:.\right]F=1\leftrightarrow E=F\right)$$