opprmulfval

Description: Value of the multiplication operation of an 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)$
	opprmulfval.4	$⊢ \underset{˙}{∙} = \cdot_{O}$
Assertion	opprmulfval	$⊢ \underset{˙}{∙} = tpos \underset{˙}{\cdot}$

Proof

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		opprmulfval.4	$⊢ \underset{˙}{∙} = \cdot_{O}$
5	1 2 3	opprval	$⊢ O = R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩$
6	5	fveq2i	$⊢ \cdot_{O} = \cdot_{(R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩)}$
7	2	fvexi	$⊢ \underset{˙}{\cdot} \in V$
8	7	tposex	$⊢ tpos \underset{˙}{\cdot} \in V$
9		mulridx	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
10	9	setsid	$⊢ (R \in V \land tpos \underset{˙}{\cdot} \in V) \to tpos \underset{˙}{\cdot} = \cdot_{(R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩)}$
11	8 10	mpan2	$⊢ R \in V \to tpos \underset{˙}{\cdot} = \cdot_{(R sSet ⟨\cdot_{ndx}, tpos \underset{˙}{\cdot}⟩)}$
12	6 11	eqtr4id	$⊢ R \in V \to \cdot_{O} = tpos \underset{˙}{\cdot}$
13		tpos0	$⊢ tpos \emptyset = \emptyset$
14	9	str0	$⊢ \emptyset = \cdot_{\emptyset}$
15	13 14	eqtr2i	$⊢ \cdot_{\emptyset} = tpos \emptyset$
16		fvprc	$⊢ \neg R \in V \to {opp}_{r} (R) = \emptyset$
17	3 16	eqtrid	$⊢ \neg R \in V \to O = \emptyset$
18	17	fveq2d	$⊢ \neg R \in V \to \cdot_{O} = \cdot_{\emptyset}$
19		fvprc	$⊢ \neg R \in V \to \cdot_{R} = \emptyset$
20	2 19	eqtrid	$⊢ \neg R \in V \to \underset{˙}{\cdot} = \emptyset$
21	20	tposeqd	$⊢ \neg R \in V \to tpos \underset{˙}{\cdot} = tpos \emptyset$
22	15 18 21	3eqtr4a	$⊢ \neg R \in V \to \cdot_{O} = tpos \underset{˙}{\cdot}$
23	12 22	pm2.61i	$⊢ \cdot_{O} = tpos \underset{˙}{\cdot}$
24	4 23	eqtri	$⊢ \underset{˙}{∙} = tpos \underset{˙}{\cdot}$

Metamath Proof Explorer

Theorem opprmulfval

Proof