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 φ E DivRing
drgext.2 φ U SubRing E
Assertion drgext0gsca φ 0 B = 0 Scalar 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 drngring E DivRing E Ring
5 ringmnd E Ring E Mnd
6 2 4 5 3syl φ E Mnd
7 subrgsubg U SubRing E U SubGrp E
8 eqid 0 E = 0 E
9 8 subg0cl U SubGrp E 0 E U
10 3 7 9 3syl φ 0 E U
11 eqid Base E = Base E
12 11 subrgss U SubRing E U Base E
13 3 12 syl φ U Base E
14 eqid E 𝑠 U = E 𝑠 U
15 14 11 8 ress0g E Mnd 0 E U U Base E 0 E = 0 E 𝑠 U
16 6 10 13 15 syl3anc φ 0 E = 0 E 𝑠 U
17 1 2 3 drgext0g φ 0 E = 0 B
18 1 a1i φ B = subringAlg E U
19 18 13 srasca φ E 𝑠 U = Scalar B
20 19 fveq2d φ 0 E 𝑠 U = 0 Scalar B
21 16 17 20 3eqtr3d φ 0 B = 0 Scalar B