This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppgval

Description: Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015) (Revised by Fan Zheng, 26-Jun-2016)

		Ref	Expression
	Hypotheses	oppgval.2	$⊢ \underset{˙}{+} = +_{R}$
		oppgval.3	$⊢ O = {opp}_{𝑔} (R)$
	Assertion	oppgval	$⊢ O = R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩$

Proof

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