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	|- ( ph -> E e. DivRing )
	drgext.2	|- ( ph -> U e. ( SubRing ` E ) )
Assertion	drgext0g	|- ( ph -> ( 0g ` E ) = ( 0g ` B ) )

Proof

Step	Hyp	Ref	Expression
1		drgext.b	|- B = ( ( subringAlg ` E ) ` U )
2		drgext.1	|- ( ph -> E e. DivRing )
3		drgext.2	|- ( ph -> U e. ( SubRing ` E ) )
4	1	a1i	|- ( ph -> B = ( ( subringAlg ` E ) ` U ) )
5		eqidd	|- ( ph -> ( 0g ` E ) = ( 0g ` E ) )
6		eqid	|- ( Base ` E ) = ( Base ` E )
7	6	subrgss	|- ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
8	3 7	syl	|- ( ph -> U C_ ( Base ` E ) )
9	4 5 8	sralmod0	|- ( ph -> ( 0g ` E ) = ( 0g ` B ) )