Metamath Proof Explorer

Theorem drgext0gsca

Description: The additive neutral element of the scalar field 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 drgext0gsca 
|- ( ph -> ( 0g ` B ) = ( 0g ` ( Scalar ` 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 drngring 
 |-  ( E e. DivRing -> E e. Ring )
5 ringmnd 
 |-  ( E e. Ring -> E e. Mnd )
6 2 4 5 3syl 
 |-  ( ph -> E e. Mnd )
7 subrgsubg 
 |-  ( U e. ( SubRing ` E ) -> U e. ( SubGrp ` E ) )
8 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
9 8 subg0cl 
 |-  ( U e. ( SubGrp ` E ) -> ( 0g ` E ) e. U )
10 3 7 9 3syl 
 |-  ( ph -> ( 0g ` E ) e. U )
11 eqid 
 |-  ( Base ` E ) = ( Base ` E )
12 11 subrgss 
 |-  ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
13 3 12 syl 
 |-  ( ph -> U C_ ( Base ` E ) )
14 eqid 
 |-  ( E |`s U ) = ( E |`s U )
15 14 11 8 ress0g 
 |-  ( ( E e. Mnd /\ ( 0g ` E ) e. U /\ U C_ ( Base ` E ) ) -> ( 0g ` E ) = ( 0g ` ( E |`s U ) ) )
16 6 10 13 15 syl3anc 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` ( E |`s U ) ) )
17 1 2 3 drgext0g 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` B ) )
18 1 a1i 
 |-  ( ph -> B = ( ( subringAlg ` E ) ` U ) )
19 18 13 srasca 
 |-  ( ph -> ( E |`s U ) = ( Scalar ` B ) )
20 19 fveq2d 
 |-  ( ph -> ( 0g ` ( E |`s U ) ) = ( 0g ` ( Scalar ` B ) ) )
21 16 17 20 3eqtr3d 
 |-  ( ph -> ( 0g ` B ) = ( 0g ` ( Scalar ` B ) ) )