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 /FldExt F -> ( ( E [:] F ) = 1 <-> E = F ) )

Proof

Step	Hyp	Ref	Expression
1		extdg1id	|- ( ( E /FldExt F /\ ( E [:] F ) = 1 ) -> E = F )
2		oveq1	|- ( E = F -> ( E [:] F ) = ( F [:] F ) )
3	2	adantl	|- ( ( E /FldExt F /\ E = F ) -> ( E [:] F ) = ( F [:] F ) )
4		fldextfld2	|- ( E /FldExt F -> F e. Field )
5	4	adantr	|- ( ( E /FldExt F /\ E = F ) -> F e. Field )
6		extdgid	|- ( F e. Field -> ( F [:] F ) = 1 )
7	5 6	syl	|- ( ( E /FldExt F /\ E = F ) -> ( F [:] F ) = 1 )
8	3 7	eqtrd	|- ( ( E /FldExt F /\ E = F ) -> ( E [:] F ) = 1 )
9	1 8	impbida	|- ( E /FldExt F -> ( ( E [:] F ) = 1 <-> E = F ) )