# Metamath Proof Explorer

## Theorem issrng

Description: The predicate "is a star ring." (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses issrng.o
`|- O = ( oppR ` R )`
issrng.i
`|- .* = ( *rf ` R )`
Assertion issrng
`|- ( R e. *Ring <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )`

### Proof

Step Hyp Ref Expression
1 issrng.o
` |-  O = ( oppR ` R )`
2 issrng.i
` |-  .* = ( *rf ` R )`
3 df-srng
` |-  *Ring = { r | [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) }`
4 3 eleq2i
` |-  ( R e. *Ring <-> R e. { r | [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) } )`
5 rhmrcl1
` |-  ( .* e. ( R RingHom O ) -> R e. Ring )`
6 5 elexd
` |-  ( .* e. ( R RingHom O ) -> R e. _V )`
` |-  ( ( .* e. ( R RingHom O ) /\ .* = `' .* ) -> R e. _V )`
8 fvexd
` |-  ( r = R -> ( *rf ` r ) e. _V )`
9 id
` |-  ( i = ( *rf ` r ) -> i = ( *rf ` r ) )`
10 fveq2
` |-  ( r = R -> ( *rf ` r ) = ( *rf ` R ) )`
11 10 2 eqtr4di
` |-  ( r = R -> ( *rf ` r ) = .* )`
12 9 11 sylan9eqr
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> i = .* )`
13 simpl
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> r = R )`
14 13 fveq2d
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( oppR ` r ) = ( oppR ` R ) )`
15 14 1 eqtr4di
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( oppR ` r ) = O )`
16 13 15 oveq12d
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( r RingHom ( oppR ` r ) ) = ( R RingHom O ) )`
17 12 16 eleq12d
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( i e. ( r RingHom ( oppR ` r ) ) <-> .* e. ( R RingHom O ) ) )`
18 12 cnveqd
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> `' i = `' .* )`
19 12 18 eqeq12d
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( i = `' i <-> .* = `' .* ) )`
20 17 19 anbi12d
` |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) ) )`
21 8 20 sbcied
` |-  ( r = R -> ( [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) ) )`
22 7 21 elab3
` |-  ( R e. { r | [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) } <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )`
23 4 22 bitri
` |-  ( R e. *Ring <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )`