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 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
drgext.1 ( 𝜑𝐸 ∈ DivRing )
drgext.2 ( 𝜑𝑈 ∈ ( SubRing ‘ 𝐸 ) )
Assertion drgext0g ( 𝜑 → ( 0g𝐸 ) = ( 0g𝐵 ) )

Proof

Step Hyp Ref Expression
1 drgext.b 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 drgext.1 ( 𝜑𝐸 ∈ DivRing )
3 drgext.2 ( 𝜑𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4 1 a1i ( 𝜑𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
5 eqidd ( 𝜑 → ( 0g𝐸 ) = ( 0g𝐸 ) )
6 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7 6 subrgss ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
8 3 7 syl ( 𝜑𝑈 ⊆ ( Base ‘ 𝐸 ) )
9 4 5 8 sralmod0 ( 𝜑 → ( 0g𝐸 ) = ( 0g𝐵 ) )