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 ) /\ .* = `' .* ) )