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 𝐻 )