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