Theorem cntrss

Description: The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023)

	Ref	Expression
Hypothesis	cntrss.1	$$⊢B={\mathrm{Base}}_M$$
Assertion	cntrss	$$⊢\mathrm{Cntr}\left(M\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		cntrss.1	$$⊢B={\mathrm{Base}}_M$$
2		eqid	$$⊢\mathrm{Cntz}\left(M\right)=\mathrm{Cntz}\left(M\right)$$
3	1 2	cntrval	$$⊢\mathrm{Cntz}\left(M\right)\left(B\right)=\mathrm{Cntr}\left(M\right)$$
4	1 2	cntzssv	$$⊢\mathrm{Cntz}\left(M\right)\left(B\right)\subseteq B$$
5	3 4	eqsstrri	$$⊢\mathrm{Cntr}\left(M\right)\subseteq B$$