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 ‘ 𝐵 ) ) )