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 eqtr4di ⊢ 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 eqtr4di ⊢ 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