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 adantr ⊢ ∗ ˙ ∈ R RingHom O ∧ ∗ ˙ = ∗ ˙ -1 → R ∈ Ring
7 fvexd ⊢ r = R → ∗ 𝑟𝑓 ⁡ r ∈ V
8 id ⊢ i = ∗ 𝑟𝑓 ⁡ r → i = ∗ 𝑟𝑓 ⁡ r
9 fveq2 ⊢ r = R → ∗ 𝑟𝑓 ⁡ r = ∗ 𝑟𝑓 ⁡ R
10 9 2 eqtr4di ⊢ r = R → ∗ 𝑟𝑓 ⁡ r = ∗ ˙
11 8 10 sylan9eqr ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → i = ∗ ˙
12 simpl ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → r = R
13 12 fveq2d ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → opp r ⁡ r = opp r ⁡ R
14 13 1 eqtr4di ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → opp r ⁡ r = O
15 12 14 oveq12d ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → r RingHom opp r ⁡ r = R RingHom O
16 11 15 eleq12d ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → i ∈ r RingHom opp r ⁡ r ↔ ∗ ˙ ∈ R RingHom O
17 11 cnveqd ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → i -1 = ∗ ˙ -1
18 11 17 eqeq12d ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → i = i -1 ↔ ∗ ˙ = ∗ ˙ -1
19 16 18 anbi12d ⊢ r = R ∧ i = ∗ 𝑟𝑓 ⁡ r → i ∈ r RingHom opp r ⁡ r ∧ i = i -1 ↔ ∗ ˙ ∈ R RingHom O ∧ ∗ ˙ = ∗ ˙ -1
20 7 19 sbcied ⊢ r = R → [˙ ∗ 𝑟𝑓 ⁡ r / i]˙ i ∈ r RingHom opp r ⁡ r ∧ i = i -1 ↔ ∗ ˙ ∈ R RingHom O ∧ ∗ ˙ = ∗ ˙ -1
21 6 20 elab3 ⊢ R ∈ r | [˙ ∗ 𝑟𝑓 ⁡ r / i]˙ i ∈ r RingHom opp r ⁡ r ∧ i = i -1 ↔ ∗ ˙ ∈ R RingHom O ∧ ∗ ˙ = ∗ ˙ -1
22 4 21 bitri ⊢ R ∈ *-Ring ↔ ∗ ˙ ∈ R RingHom O ∧ ∗ ˙ = ∗ ˙ -1