Metamath Proof Explorer


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 = ( Base ` M )
Assertion cntrss
|- ( Cntr ` M ) C_ B

Proof

Step Hyp Ref Expression
1 cntrss.1
 |-  B = ( Base ` M )
2 eqid
 |-  ( Cntz ` M ) = ( Cntz ` M )
3 1 2 cntrval
 |-  ( ( Cntz ` M ) ` B ) = ( Cntr ` M )
4 1 2 cntzssv
 |-  ( ( Cntz ` M ) ` B ) C_ B
5 3 4 eqsstrri
 |-  ( Cntr ` M ) C_ B