Theorem fldextsdrg

Description: Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	fldextsdrg.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
	fldextsdrg.2	⊢ ( 𝜑 → 𝐸 /FldExt 𝐹 )
Assertion	fldextsdrg	⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		fldextsdrg.1	⊢ 𝐵 = ( Base ‘ 𝐹 )
2		fldextsdrg.2	⊢ ( 𝜑 → 𝐸 /FldExt 𝐹 )
3		fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
4	2 3	syl	⊢ ( 𝜑 → 𝐸 ∈ Field )
5	4	flddrngd	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
6	1	fldextsubrg	⊢ ( 𝐸 /FldExt 𝐹 → 𝐵 ∈ ( SubRing ‘ 𝐸 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝐸 ) )
8		fldextress	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
9	2 8	syl	⊢ ( 𝜑 → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
10	1	oveq2i	⊢ ( 𝐸 ↾s 𝐵 ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) )
11	9 10	eqtr4di	⊢ ( 𝜑 → 𝐹 = ( 𝐸 ↾s 𝐵 ) )
12		fldextfld2	⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
13	2 12	syl	⊢ ( 𝜑 → 𝐹 ∈ Field )
14	11 13	eqeltrrd	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐵 ) ∈ Field )
15	14	flddrngd	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐵 ) ∈ DivRing )
16		issdrg	⊢ ( 𝐵 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐵 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐵 ) ∈ DivRing ) )
17	5 7 15 16	syl3anbrc	⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐸 ) )