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

Metamath Proof Explorer

Theorem fldsdrgfldext

Description: A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses fldsdrgfldext.1 ⊢ 𝐺 = ( 𝐹 ↾s 𝐴 )
fldsdrgfldext.2 ⊢ ( 𝜑 → 𝐹 ∈ Field )
fldsdrgfldext.3 ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝐹 ) )
Assertion fldsdrgfldext ( 𝜑 → 𝐹 /FldExt 𝐺 )

Proof

Step Hyp Ref Expression
1 fldsdrgfldext.1 ⊢ 𝐺 = ( 𝐹 ↾s 𝐴 )
2 fldsdrgfldext.2 ⊢ ( 𝜑 → 𝐹 ∈ Field )
3 fldsdrgfldext.3 ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝐹 ) )
4 fldsdrgfld ⊢ ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ Field )
5 2 3 4 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾s 𝐴 ) ∈ Field )
6 1 5 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ Field )
7 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8 7 sdrgss ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) → 𝐴 ⊆ ( Base ‘ 𝐹 ) )
9 1 7 ressbas2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐹 ) → 𝐴 = ( Base ‘ 𝐺 ) )
10 3 8 9 3syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝐺 ) )
11 10 oveq2d ⊢ ( 𝜑 → ( 𝐹 ↾s 𝐴 ) = ( 𝐹 ↾s ( Base ‘ 𝐺 ) ) )
12 1 11 eqtrid ⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾s ( Base ‘ 𝐺 ) ) )
13 sdrgsubrg ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) → 𝐴 ∈ ( SubRing ‘ 𝐹 ) )
14 3 13 syl ⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝐹 ) )
15 10 14 eqeltrrd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ∈ ( SubRing ‘ 𝐹 ) )
16 brfldext ⊢ ( ( 𝐹 ∈ Field ∧ 𝐺 ∈ Field ) → ( 𝐹 /FldExt 𝐺 ↔ ( 𝐺 = ( 𝐹 ↾s ( Base ‘ 𝐺 ) ) ∧ ( Base ‘ 𝐺 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
17 16 biimpar ⊢ ( ( ( 𝐹 ∈ Field ∧ 𝐺 ∈ Field ) ∧ ( 𝐺 = ( 𝐹 ↾s ( Base ‘ 𝐺 ) ) ∧ ( Base ‘ 𝐺 ) ∈ ( SubRing ‘ 𝐹 ) ) ) → 𝐹 /FldExt 𝐺 )
18 2 6 12 15 17 syl22anc ⊢ ( 𝜑 → 𝐹 /FldExt 𝐺 )