# 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}={opp}_{r}\left({R}\right)$
issrng.i
Assertion issrng

### Proof

Step Hyp Ref Expression
1 issrng.o ${⊢}{O}={opp}_{r}\left({R}\right)$
2 issrng.i
3 df-srng
4 3 eleq2i
5 rhmrcl1
6 5 elexd
8 fvexd ${⊢}{r}={R}\to {\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\in \mathrm{V}$
9 id ${⊢}{i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\to {i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)$
10 fveq2 ${⊢}{r}={R}\to {\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)={\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)$
11 10 2 syl6eqr
12 9 11 sylan9eqr
13 simpl ${⊢}\left({r}={R}\wedge {i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\right)\to {r}={R}$
14 13 fveq2d ${⊢}\left({r}={R}\wedge {i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\right)\to {opp}_{r}\left({r}\right)={opp}_{r}\left({R}\right)$
15 14 1 syl6eqr ${⊢}\left({r}={R}\wedge {i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\right)\to {opp}_{r}\left({r}\right)={O}$
16 13 15 oveq12d ${⊢}\left({r}={R}\wedge {i}={\ast }_{\mathrm{𝑟𝑓}}\left({r}\right)\right)\to {r}\mathrm{RingHom}{opp}_{r}\left({r}\right)={R}\mathrm{RingHom}{O}$
17 12 16 eleq12d
18 12 cnveqd
19 12 18 eqeq12d
20 17 19 anbi12d
21 8 20 sbcied
22 7 21 elab3
23 4 22 bitri