This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unitcl

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses unitcl.1 
|- B = ( Base ` R )
unitcl.2 
|- U = ( Unit ` R )
Assertion unitcl 
|- ( X e. U -> X e. B )

Proof

Step Hyp Ref Expression
1 unitcl.1 
 |-  B = ( Base ` R )
2 unitcl.2 
 |-  U = ( Unit ` R )
3 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
4 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
5 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
6 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
7 2 3 4 5 6 isunit 
 |-  ( X e. U <-> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
8 7 simplbi 
 |-  ( X e. U -> X ( ||r ` R ) ( 1r ` R ) )
9 1 4 dvdsrcl 
 |-  ( X ( ||r ` R ) ( 1r ` R ) -> X e. B )
10 8 9 syl 
 |-  ( X e. U -> X e. B )