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

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