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

Metamath Proof Explorer

Theorem srngf1o

Description: The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcnv.i 
|- .* = ( *rf ` R )
srngf1o.b 
|- B = ( Base ` R )
Assertion srngf1o 
|- ( R e. *Ring -> .* : B -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 srngcnv.i 
 |-  .* = ( *rf ` R )
2 srngf1o.b 
 |-  B = ( Base ` R )
3 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
4 3 1 srngrhm 
 |-  ( R e. *Ring -> .* e. ( R RingHom ( oppR ` R ) ) )
5 eqid 
 |-  ( Base ` ( oppR ` R ) ) = ( Base ` ( oppR ` R ) )
6 2 5 rhmf 
 |-  ( .* e. ( R RingHom ( oppR ` R ) ) -> .* : B --> ( Base ` ( oppR ` R ) ) )
7 ffn 
 |-  ( .* : B --> ( Base ` ( oppR ` R ) ) -> .* Fn B )
8 4 6 7 3syl 
 |-  ( R e. *Ring -> .* Fn B )
9 1 srngcnv 
 |-  ( R e. *Ring -> .* = `' .* )
10 9 fneq1d 
 |-  ( R e. *Ring -> ( .* Fn B <-> `' .* Fn B ) )
11 8 10 mpbid 
 |-  ( R e. *Ring -> `' .* Fn B )
12 dff1o4 
 |-  ( .* : B -1-1-onto-> B <-> ( .* Fn B /\ `' .* Fn B ) )
13 8 11 12 sylanbrc 
 |-  ( R e. *Ring -> .* : B -1-1-onto-> B )