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

Metamath Proof Explorer

Theorem sdrgfldext

Description: A field E and any sub-division-ring F of E form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses sdrgfldext.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
sdrgfldext.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
sdrgfldext.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
Assertion sdrgfldext ( 𝜑 → 𝐸 /FldExt ( 𝐸 ↾s 𝐹 ) )

Proof

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