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