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	$⊢ \underset{˙}{} = _{𝑟𝑓} (R)$
Assertion	issrng	$⊢ R \in -Ring \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		issrng.o	$⊢ O = {opp}_{r} (R)$
2		issrng.i	$⊢ \underset{˙}{} = _{𝑟𝑓} (R)$
3		df-srng	$⊢ -Ring = \{r \| \underset{˙}{[} _{𝑟𝑓} (r) / i \underset{˙}{]} (i \in (r RingHom {opp}_{r} (r)) \land i = i^{-1})\}$
4	3	eleq2i	$⊢ R \in -Ring \leftrightarrow R \in \{r \| \underset{˙}{[} _{𝑟𝑓} (r) / i \underset{˙}{]} (i \in (r RingHom {opp}_{r} (r)) \land i = i^{-1})\}$
5		rhmrcl1	$⊢ \underset{˙}{*} \in (R RingHom O) \to R \in Ring$
6	5	adantr	$⊢ (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{*}}^{-1}) \to R \in Ring$
7		fvexd	$⊢ r = R \to *_{𝑟𝑓} (r) \in V$
8		id	$⊢ i = _{𝑟𝑓} (r) \to i = _{𝑟𝑓} (r)$
9		fveq2	$⊢ r = R \to _{𝑟𝑓} (r) = _{𝑟𝑓} (R)$
10	9 2	eqtr4di	$⊢ r = R \to _{𝑟𝑓} (r) = \underset{˙}{}$
11	8 10	sylan9eqr	$⊢ (r = R \land i = _{𝑟𝑓} (r)) \to i = \underset{˙}{}$
12		simpl	$⊢ (r = R \land i = *_{𝑟𝑓} (r)) \to r = R$
13	12	fveq2d	$⊢ (r = R \land i = *_{𝑟𝑓} (r)) \to {opp}_{r} (r) = {opp}_{r} (R)$
14	13 1	eqtr4di	$⊢ (r = R \land i = *_{𝑟𝑓} (r)) \to {opp}_{r} (r) = O$
15	12 14	oveq12d	$⊢ (r = R \land i = *_{𝑟𝑓} (r)) \to r RingHom {opp}_{r} (r) = R RingHom O$
16	11 15	eleq12d	$⊢ (r = R \land i = _{𝑟𝑓} (r)) \to (i \in (r RingHom {opp}_{r} (r)) \leftrightarrow \underset{˙}{} \in (R RingHom O))$
17	11	cnveqd	$⊢ (r = R \land i = _{𝑟𝑓} (r)) \to i^{-1} = {\underset{˙}{}}^{-1}$
18	11 17	eqeq12d	$⊢ (r = R \land i = _{𝑟𝑓} (r)) \to (i = i^{-1} \leftrightarrow \underset{˙}{} = {\underset{˙}{*}}^{-1})$
19	16 18	anbi12d	$⊢ (r = R \land i = _{𝑟𝑓} (r)) \to ((i \in (r RingHom {opp}_{r} (r)) \land i = i^{-1}) \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1}))$
20	7 19	sbcied	$⊢ r = R \to (\underset{˙}{[} _{𝑟𝑓} (r) / i \underset{˙}{]} (i \in (r RingHom {opp}_{r} (r)) \land i = i^{-1}) \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1}))$
21	6 20	elab3	$⊢ R \in \{r \| \underset{˙}{[} _{𝑟𝑓} (r) / i \underset{˙}{]} (i \in (r RingHom {opp}_{r} (r)) \land i = i^{-1})\} \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1})$
22	4 21	bitri	$⊢ R \in -Ring \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1})$

Metamath Proof Explorer

Theorem issrng

Proof