Theorem opprmulfval

Description: Value of the multiplication operation of an 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)$$
	opprmulfval.4	$$⊢\underset{\dot{}}{\bullet }={\cdot }_O$$
Assertion	opprmulfval	$$⊢\underset{\dot{}}{\bullet }=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		opprmulfval.4	$$⊢\underset{\dot{}}{\bullet }={\cdot }_O$$
5	1 2 3	opprval	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩$$
6	5	fveq2i	$$⊢{\cdot }_O={\cdot }_{\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)}$$
7	2	fvexi	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
8	7	tposex	$$⊢tpos\underset{\dot{}}{·}\in \mathrm{V}$$
9		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
10	9	setsid	$$⊢\left(R\in \mathrm{V}\wedge tpos\underset{\dot{}}{·}\in \mathrm{V}\right)\to tpos\underset{\dot{}}{·}={\cdot }_{\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)}$$
11	8 10	mpan2	$$⊢R\in \mathrm{V}\to tpos\underset{\dot{}}{·}={\cdot }_{\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos\underset{\dot{}}{·}⟩\right)}$$
12	6 11	eqtr4id	$$⊢R\in \mathrm{V}\to {\cdot }_O=tpos\underset{\dot{}}{·}$$
13		tpos0	$$⊢tpos\varnothing =\varnothing$$
14	9	str0	$$⊢\varnothing ={\cdot }_{\varnothing }$$
15	13 14	eqtr2i	$$⊢{\cdot }_{\varnothing }=tpos\varnothing$$
16		fvprc	$$⊢\neg R\in \mathrm{V}\to {opp}_r\left(R\right)=\varnothing$$
17	3 16	eqtrid	$$⊢\neg R\in \mathrm{V}\to O=\varnothing$$
18	17	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\cdot }_O={\cdot }_{\varnothing }$$
19		fvprc	$$⊢\neg R\in \mathrm{V}\to {\cdot }_R=\varnothing$$
20	2 19	eqtrid	$$⊢\neg R\in \mathrm{V}\to \underset{\dot{}}{·}=\varnothing$$
21	20	tposeqd	$$⊢\neg R\in \mathrm{V}\to tpos\underset{\dot{}}{·}=tpos\varnothing$$
22	15 18 21	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {\cdot }_O=tpos\underset{\dot{}}{·}$$
23	12 22	pm2.61i	$$⊢{\cdot }_O=tpos\underset{\dot{}}{·}$$
24	4 23	eqtri	$$⊢\underset{\dot{}}{\bullet }=tpos\underset{\dot{}}{·}$$