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	⊢ ( 𝐸 /FldExt 𝐹 → ( ( 𝐸 [:] 𝐹 ) = 1 ↔ 𝐸 = 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		extdg1id	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 1 ) → 𝐸 = 𝐹 )
2		oveq1	⊢ ( 𝐸 = 𝐹 → ( 𝐸 [:] 𝐹 ) = ( 𝐹 [:] 𝐹 ) )
3	2	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐸 = 𝐹 ) → ( 𝐸 [:] 𝐹 ) = ( 𝐹 [:] 𝐹 ) )
4		fldextfld2	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
5	4	adantr	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐸 = 𝐹 ) → 𝐹 ∈ Field )
6		extdgid	⊢ ( 𝐹 ∈ Field → ( 𝐹 [:] 𝐹 ) = 1 )
7	5 6	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐸 = 𝐹 ) → ( 𝐹 [:] 𝐹 ) = 1 )
8	3 7	eqtrd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐸 = 𝐹 ) → ( 𝐸 [:] 𝐹 ) = 1 )
9	1 8	impbida	⊢ ( 𝐸 /FldExt 𝐹 → ( ( 𝐸 [:] 𝐹 ) = 1 ↔ 𝐸 = 𝐹 ) )