Theorem drgextsubrg

Description: The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

	Ref	Expression
Hypotheses	drgext.b	⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
	drgext.1	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
	drgext.2	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
	drgext.f	⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
	drgext.3	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion	drgextsubrg	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		drgext.b	⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2		drgext.1	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
3		drgext.2	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4		drgext.f	⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
5		drgext.3	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
6	1	a1i	⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
7		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8	7	subrgss	⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
9	3 8	syl	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
10	6 3 9	srasubrg	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐵 ) )