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

Metamath Proof Explorer

Theorem fldsdrgfldext2

Description: A sub-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 ‘ 𝐹 ) )
fldsdrgfldext2.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐺 ) )
fldsdrgfldext2.h ⊢ 𝐻 = ( 𝐹 ↾s 𝐵 )
Assertion fldsdrgfldext2 ( 𝜑 → 𝐺 /FldExt 𝐻 )

Proof

Step Hyp Ref Expression
1 fldsdrgfldext.1 ⊢ 𝐺 = ( 𝐹 ↾s 𝐴 )
2 fldsdrgfldext.2 ⊢ ( 𝜑 → 𝐹 ∈ Field )
3 fldsdrgfldext.3 ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝐹 ) )
4 fldsdrgfldext2.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐺 ) )
5 fldsdrgfldext2.h ⊢ 𝐻 = ( 𝐹 ↾s 𝐵 )
6 eqid ⊢ ( 𝐺 ↾s 𝐵 ) = ( 𝐺 ↾s 𝐵 )
7 fldsdrgfld ⊢ ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ Field )
8 2 3 7 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾s 𝐴 ) ∈ Field )
9 1 8 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ Field )
10 6 9 4 fldsdrgfldext ⊢ ( 𝜑 → 𝐺 /FldExt ( 𝐺 ↾s 𝐵 ) )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 11 sdrgss ⊢ ( 𝐵 ∈ ( SubDRing ‘ 𝐺 ) → 𝐵 ⊆ ( Base ‘ 𝐺 ) )
13 4 12 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝐺 ) )
14 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
15 14 sdrgss ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) → 𝐴 ⊆ ( Base ‘ 𝐹 ) )
16 1 14 ressbas2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝐹 ) → 𝐴 = ( Base ‘ 𝐺 ) )
17 3 15 16 3syl ⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝐺 ) )
18 13 17 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
19 ressabs ⊢ ( ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝐹 ↾s 𝐵 ) )
20 3 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝐹 ↾s 𝐵 ) )
21 1 oveq1i ⊢ ( 𝐺 ↾s 𝐵 ) = ( ( 𝐹 ↾s 𝐴 ) ↾s 𝐵 )
22 20 21 5 3eqtr4g ⊢ ( 𝜑 → ( 𝐺 ↾s 𝐵 ) = 𝐻 )
23 10 22 breqtrd ⊢ ( 𝜑 → 𝐺 /FldExt 𝐻 )