oppgplusfval

Description: Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Fan Zheng, 26-Jun-2016)

	Ref	Expression
Hypotheses	oppgval.2	$⊢ \underset{˙}{+} = +_{R}$
	oppgval.3	$⊢ O = {opp}_{𝑔} (R)$
	oppgplusfval.4	$⊢ \underset{˙}{✚} = +_{O}$
Assertion	oppgplusfval	$⊢ \underset{˙}{✚} = tpos \underset{˙}{+}$

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	$⊢ \underset{˙}{+} = +_{R}$
2		oppgval.3	$⊢ O = {opp}_{𝑔} (R)$
3		oppgplusfval.4	$⊢ \underset{˙}{✚} = +_{O}$
4	1 2	oppgval	$⊢ O = R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩$
5	4	fveq2i	$⊢ +_{O} = +_{(R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩)}$
6	1	fvexi	$⊢ \underset{˙}{+} \in V$
7	6	tposex	$⊢ tpos \underset{˙}{+} \in V$
8		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
9	8	setsid	$⊢ (R \in V \land tpos \underset{˙}{+} \in V) \to tpos \underset{˙}{+} = +_{(R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩)}$
10	7 9	mpan2	$⊢ R \in V \to tpos \underset{˙}{+} = +_{(R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩)}$
11	5 10	eqtr4id	$⊢ R \in V \to +_{O} = tpos \underset{˙}{+}$
12		tpos0	$⊢ tpos \emptyset = \emptyset$
13	8	str0	$⊢ \emptyset = +_{\emptyset}$
14	12 13	eqtr2i	$⊢ +_{\emptyset} = tpos \emptyset$
15		reldmsets	$⊢ Rel dom sSet$
16	15	ovprc1	$⊢ \neg R \in V \to R sSet ⟨+_{ndx}, tpos \underset{˙}{+}⟩ = \emptyset$
17	4 16	eqtrid	$⊢ \neg R \in V \to O = \emptyset$
18	17	fveq2d	$⊢ \neg R \in V \to +_{O} = +_{\emptyset}$
19		fvprc	$⊢ \neg R \in V \to +_{R} = \emptyset$
20	1 19	eqtrid	$⊢ \neg R \in V \to \underset{˙}{+} = \emptyset$
21	20	tposeqd	$⊢ \neg R \in V \to tpos \underset{˙}{+} = tpos \emptyset$
22	14 18 21	3eqtr4a	$⊢ \neg R \in V \to +_{O} = tpos \underset{˙}{+}$
23	11 22	pm2.61i	$⊢ +_{O} = tpos \underset{˙}{+}$
24	3 23	eqtri	$⊢ \underset{˙}{✚} = tpos \underset{˙}{+}$

Metamath Proof Explorer

Theorem oppgplusfval

Proof