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 )`