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 R
issrng.i ˙ = 𝑟𝑓 R
Assertion issrng R *-Ring ˙ R RingHom O ˙ = ˙ -1

Proof

Step Hyp Ref Expression
1 issrng.o O = opp r R
2 issrng.i ˙ = 𝑟𝑓 R
3 df-srng *-Ring = r | [˙ 𝑟𝑓 r / i]˙ i r RingHom opp r r i = i -1
4 3 eleq2i R *-Ring R r | [˙ 𝑟𝑓 r / i]˙ i r RingHom opp r r i = i -1
5 rhmrcl1 ˙ R RingHom O R Ring
6 5 elexd ˙ R RingHom O R V
7 6 adantr ˙ R RingHom O ˙ = ˙ -1 R V
8 fvexd r = R 𝑟𝑓 r V
9 id i = 𝑟𝑓 r i = 𝑟𝑓 r
10 fveq2 r = R 𝑟𝑓 r = 𝑟𝑓 R
11 10 2 syl6eqr r = R 𝑟𝑓 r = ˙
12 9 11 sylan9eqr r = R i = 𝑟𝑓 r i = ˙
13 simpl r = R i = 𝑟𝑓 r r = R
14 13 fveq2d r = R i = 𝑟𝑓 r opp r r = opp r R
15 14 1 syl6eqr r = R i = 𝑟𝑓 r opp r r = O
16 13 15 oveq12d r = R i = 𝑟𝑓 r r RingHom opp r r = R RingHom O
17 12 16 eleq12d r = R i = 𝑟𝑓 r i r RingHom opp r r ˙ R RingHom O
18 12 cnveqd r = R i = 𝑟𝑓 r i -1 = ˙ -1
19 12 18 eqeq12d r = R i = 𝑟𝑓 r i = i -1 ˙ = ˙ -1
20 17 19 anbi12d r = R i = 𝑟𝑓 r i r RingHom opp r r i = i -1 ˙ R RingHom O ˙ = ˙ -1
21 8 20 sbcied r = R [˙ 𝑟𝑓 r / i]˙ i r RingHom opp r r i = i -1 ˙ R RingHom O ˙ = ˙ -1
22 7 21 elab3 R r | [˙ 𝑟𝑓 r / i]˙ i r RingHom opp r r i = i -1 ˙ R RingHom O ˙ = ˙ -1
23 4 22 bitri R *-Ring ˙ R RingHom O ˙ = ˙ -1