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

Metamath Proof Explorer

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 ⊢ B = subringAlg ⁡ E ⁡ U
drgext.1 ⊢ φ → E ∈ DivRing
drgext.2 ⊢ φ → U ∈ SubRing ⁡ E
drgext.f ⊢ F = E ↾ 𝑠 U
drgext.3 ⊢ φ → F ∈ DivRing
Assertion drgextsubrg ⊢ φ → U ∈ SubRing ⁡ B

Proof

Step Hyp Ref Expression
1 drgext.b ⊢ B = subringAlg ⁡ E ⁡ U
2 drgext.1 ⊢ φ → E ∈ DivRing
3 drgext.2 ⊢ φ → U ∈ SubRing ⁡ E
4 drgext.f ⊢ F = E ↾ 𝑠 U
5 drgext.3 ⊢ φ → F ∈ DivRing
6 1 a1i ⊢ φ → B = subringAlg ⁡ E ⁡ U
7 eqid ⊢ Base E = Base E
8 7 subrgss ⊢ U ∈ SubRing ⁡ E → U ⊆ Base E
9 3 8 syl ⊢ φ → U ⊆ Base E
10 6 3 9 srasubrg ⊢ φ → U ∈ SubRing ⁡ B