Theorem opprval

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

	Ref	Expression
Hypotheses	opprval.1	$$⊢B={\mathrm{Base}}_R$$
	opprval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	opprval.3	$$⊢O={opp}_r\left(R\right)$$
Assertion	opprval	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$

Proof

Step	Hyp	Ref	Expression
1		opprval.1	$$⊢B={\mathrm{Base}}_R$$
2		opprval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		opprval.3	$$⊢O={opp}_r\left(R\right)$$
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{\dot{}}{·}$$
7	6	tposeqd	$$⊢x=R\to tpos{\cdot }_x=tpos\underset{\dot{}}{·}$$
8	7	opeq2d	$$⊢x=R\to ⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_x⟩=⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
9	4 8	oveq12d	$$⊢x=R\to x\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_x⟩=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
10		df-oppr	$$⊢{opp}_r=\left(x\in \mathrm{V}⟼x\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_x⟩\right)$$
11		ovex	$$⊢R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\in \mathrm{V}$$
12	9 10 11	fvmpt	$$⊢R\in \mathrm{V}\to {opp}_r\left(R\right)=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
13		fvprc	$$⊢\neg R\in \mathrm{V}\to {opp}_r\left(R\right)=\varnothing$$
14		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
15	14	ovprc1	$$⊢\neg R\in \mathrm{V}\to R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩=\varnothing$$
16	13 15	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {opp}_r\left(R\right)=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
17	12 16	pm2.61i	$$⊢{opp}_r\left(R\right)=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
18	3 17	eqtri	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$