opprval

Description: Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprval.1	$⊢ B = {Base}_{R}$
	opprval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	opprval.3	$⊢ O = {opp}_{r} (R)$
Assertion	opprval	$⊢ O = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$

Step	Hyp	Ref	Expression
1		opprval.1	$⊢ B = {Base}_{R}$
2		opprval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		opprval.3	$⊢ O = {opp}_{r} (R)$
4		id	$⊢ x = R \to x = R$
5		fveq2	$⊢ x = R \to \cdot_{x} = \cdot_{R}$
6	5 2	eqtr4di	$⊢ x = R \to \cdot_{x} = \underset{˙}{\cdot}$
7	6	tposeqd	$⊢ x = R \to tpos \cdot_{x} = tpos \underset{˙}{\cdot}$
8	7	opeq2d	$⊢ x = R \to ⟨\cdot_{ndx}, tpos \cdot_{x}⟩ = ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
9	4 8	oveq12d	$⊢ x = R \to x sSet ⟨\cdot_{ndx}, tpos \cdot_{x}⟩ = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
10		df-oppr	$⊢ {opp}_{r} = (x \in V ⟼ x sSet ⟨\cdot_{ndx}, tpos \cdot_{x}⟩)$
11		ovex	$⊢ R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩ \in V$
12	9 10 11	fvmpt	$⊢ R \in V \to {opp}_{r} (R) = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
13		fvprc	$⊢ \neg R \in V \to {opp}_{r} (R) = \emptyset$
14		reldmsets	$⊢ Rel dom sSet$
15	14	ovprc1	$⊢ \neg R \in V \to R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩ = \emptyset$
16	13 15	eqtr4d	$⊢ \neg R \in V \to {opp}_{r} (R) = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
17	12 16	pm2.61i	$⊢ {opp}_{r} (R) = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
18	3 17	eqtri	$⊢ O = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$

Metamath Proof Explorer