This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↔ 𝐸 = 𝐹 ) )