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 adantr
 |-  ( ( .* e. ( R RingHom O ) /\ .* = `' .* ) -> R e. Ring )
7 fvexd
 |-  ( r = R -> ( *rf ` r ) e. _V )
8 id
 |-  ( i = ( *rf ` r ) -> i = ( *rf ` r ) )
9 fveq2
 |-  ( r = R -> ( *rf ` r ) = ( *rf ` R ) )
10 9 2 eqtr4di
 |-  ( r = R -> ( *rf ` r ) = .* )
11 8 10 sylan9eqr
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> i = .* )
12 simpl
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> r = R )
13 12 fveq2d
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( oppR ` r ) = ( oppR ` R ) )
14 13 1 eqtr4di
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( oppR ` r ) = O )
15 12 14 oveq12d
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( r RingHom ( oppR ` r ) ) = ( R RingHom O ) )
16 11 15 eleq12d
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( i e. ( r RingHom ( oppR ` r ) ) <-> .* e. ( R RingHom O ) ) )
17 11 cnveqd
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> `' i = `' .* )
18 11 17 eqeq12d
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( i = `' i <-> .* = `' .* ) )
19 16 18 anbi12d
 |-  ( ( r = R /\ i = ( *rf ` r ) ) -> ( ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) ) )
20 7 19 sbcied
 |-  ( r = R -> ( [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) ) )
21 6 20 elab3
 |-  ( R e. { r | [. ( *rf ` r ) / i ]. ( i e. ( r RingHom ( oppR ` r ) ) /\ i = `' i ) } <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )
22 4 21 bitri
 |-  ( R e. *Ring <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )