Theorem opprabs

Description: The opposite ring of the opposite ring is the original ring. Note the conditions on this theorem, which makes it unpractical in case we only have e.g. R e. Ring as a premise. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	opprabs.o	$$⊢O={opp}_r\left(R\right)$$
	opprabs.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	opprabs.1	$$⊢\phi \to R\in V$$
	opprabs.2	$$⊢\phi \to \mathrm{Fun}R$$
	opprabs.3	$$⊢\phi \to {\cdot }_{\mathrm{ndx}}\in \mathrm{dom}R$$
	opprabs.4	$$⊢\phi \to \underset{\dot{}}{·}Fn\left(B\times B\right)$$
Assertion	opprabs	$$⊢\phi \to R={opp}_r\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		opprabs.o	$$⊢O={opp}_r\left(R\right)$$
2		opprabs.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		opprabs.1	$$⊢\phi \to R\in V$$
4		opprabs.2	$$⊢\phi \to \mathrm{Fun}R$$
5		opprabs.3	$$⊢\phi \to {\cdot }_{\mathrm{ndx}}\in \mathrm{dom}R$$
6		opprabs.4	$$⊢\phi \to \underset{\dot{}}{·}Fn\left(B\times B\right)$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢{\cdot }_O={\cdot }_O$$
9	7 2 1 8	opprmulfval	$$⊢{\cdot }_O=tpos\underset{\dot{}}{·}$$
10	9	tposeqi	$$⊢tpos{\cdot }_O=tpostpos\underset{\dot{}}{·}$$
11		fnrel	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to \mathrm{Rel}\underset{\dot{}}{·}$$
12		relxp	$$⊢\mathrm{Rel}\left(B\times B\right)$$
13		fndm	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to \mathrm{dom}\underset{\dot{}}{·}=B\times B$$
14	13	releqd	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to \left(\mathrm{Rel}\mathrm{dom}\underset{\dot{}}{·}\leftrightarrow \mathrm{Rel}\left(B\times B\right)\right)$$
15	12 14	mpbiri	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to \mathrm{Rel}\mathrm{dom}\underset{\dot{}}{·}$$
16		tpostpos2	$$⊢\left(\mathrm{Rel}\underset{\dot{}}{·}\wedge \mathrm{Rel}\mathrm{dom}\underset{\dot{}}{·}\right)\to tpostpos\underset{\dot{}}{·}=\underset{\dot{}}{·}$$
17	11 15 16	syl2anc	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to tpostpos\underset{\dot{}}{·}=\underset{\dot{}}{·}$$
18	10 17	eqtrid	$$⊢\underset{\dot{}}{·}Fn\left(B\times B\right)\to tpos{\cdot }_O=\underset{\dot{}}{·}$$
19	6 18	syl	$$⊢\phi \to tpos{\cdot }_O=\underset{\dot{}}{·}$$
20	19 2	eqtrdi	$$⊢\phi \to tpos{\cdot }_O={\cdot }_R$$
21	20	opeq2d	$$⊢\phi \to ⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩=⟨{\cdot }_{\mathrm{ndx}},{\cdot }_R⟩$$
22	21	oveq2d	$$⊢\phi \to R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_R⟩$$
23	1 7	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
24		eqid	$$⊢{opp}_r\left(O\right)={opp}_r\left(O\right)$$
25	23 8 24	opprval	$$⊢{opp}_r\left(O\right)=O\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
26	7 2 1	opprval	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
27	26	oveq1i	$$⊢O\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩=\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
28	25 27	eqtri	$$⊢{opp}_r\left(O\right)=\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
29		fvex	$$⊢{\cdot }_O\in \mathrm{V}$$
30	29	tposex	$$⊢tpos{\cdot }_O\in \mathrm{V}$$
31		setsabs	$$⊢\left(R\in V\wedge tpos{\cdot }_O\in \mathrm{V}\right)\to \left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
32	30 31	mpan2	$$⊢R\in V\to \left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
33	28 32	eqtrid	$$⊢R\in V\to {opp}_r\left(O\right)=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
34	3 33	syl	$$⊢\phi \to {opp}_r\left(O\right)=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_O⟩$$
35		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
36	35 3 4 5	setsidvald	$$⊢\phi \to R=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_R⟩$$
37	22 34 36	3eqtr4rd	$$⊢\phi \to R={opp}_r\left(O\right)$$