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

Metamath Proof Explorer

Theorem fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion fldextid ( 𝐹 ∈ Field → 𝐹 /FldExt 𝐹 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
2 1 ressid ⊢ ( 𝐹 ∈ Field → ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) = 𝐹 )
3 2 eqcomd ⊢ ( 𝐹 ∈ Field → 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) )
4 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
5 4 simplbi ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
6 drngring ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
7 1 subrgid ⊢ ( 𝐹 ∈ Ring → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
8 5 6 7 3syl ⊢ ( 𝐹 ∈ Field → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) )
9 brfldext ⊢ ( ( 𝐹 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐹 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
10 9 anidms ⊢ ( 𝐹 ∈ Field → ( 𝐹 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐹 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
11 3 8 10 mpbir2and ⊢ ( 𝐹 ∈ Field → 𝐹 /FldExt 𝐹 )