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

Proof

Step Hyp Ref Expression
1 drgext.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 drgext.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
3 drgext.2 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4 drngring ⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ Ring )
5 ringmnd ⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ Mnd )
6 2 4 5 3syl ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
7 subrgsubg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ∈ ( SubGrp ‘ 𝐸 ) )
8 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
9 8 subg0cl ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ 𝑈 )
10 3 7 9 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝑈 )
11 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
12 11 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
13 3 12 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
14 eqid ⊢ ( 𝐸 ↾s 𝑈 ) = ( 𝐸 ↾s 𝑈 )
15 14 11 8 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ 𝑈 ∧ 𝑈 ⊆ ( Base ‘ 𝐸 ) ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝑈 ) ) )
16 6 10 13 15 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝑈 ) ) )
17 1 2 3 drgext0g ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) )
18 1 a1i ⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
19 18 13 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑈 ) = ( Scalar ‘ 𝐵 ) )
20 19 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( 𝐸 ↾s 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )
21 16 17 20 3eqtr3d ⊢ ( 𝜑 → ( 0g ‘ 𝐵 ) = ( 0g ‘ ( Scalar ‘ 𝐵 ) ) )