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

Metamath Proof Explorer

Theorem drgext0g

Description: The additive neutral element 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
Assertion drgext0g ⊢ φ → 0 E = 0 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 1 a1i ⊢ φ → B = subringAlg ⁡ E ⁡ U
5 eqidd ⊢ φ → 0 E = 0 E
6 eqid ⊢ Base E = Base E
7 6 subrgss ⊢ U ∈ SubRing ⁡ E → U ⊆ Base E
8 3 7 syl ⊢ φ → U ⊆ Base E
9 4 5 8 sralmod0 ⊢ φ → 0 E = 0 B