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