mgpplusg

Description: Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014)

Step	Hyp	Ref	Expression
1		mgpval.1	$⊢ M = {mulGrp}_{R}$
2		mgpval.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3	2	fvexi	$⊢ \underset{˙}{\cdot} \in V$
4		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
5	4	setsid	$⊢ (R \in V \land \underset{˙}{\cdot} \in V) \to \underset{˙}{\cdot} = +_{(R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩)}$
6	3 5	mpan2	$⊢ R \in V \to \underset{˙}{\cdot} = +_{(R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩)}$
7	1 2	mgpval	$⊢ M = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
8	7	fveq2i	$⊢ +_{M} = +_{(R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩)}$
9	6 8	eqtr4di	$⊢ R \in V \to \underset{˙}{\cdot} = +_{M}$
10	4	str0	$⊢ \emptyset = +_{\emptyset}$
11		fvprc	$⊢ \neg R \in V \to \cdot_{R} = \emptyset$
12	2 11	eqtrid	$⊢ \neg R \in V \to \underset{˙}{\cdot} = \emptyset$
13		fvprc	$⊢ \neg R \in V \to {mulGrp}_{R} = \emptyset$
14	1 13	eqtrid	$⊢ \neg R \in V \to M = \emptyset$
15	14	fveq2d	$⊢ \neg R \in V \to +_{M} = +_{\emptyset}$
16	10 12 15	3eqtr4a	$⊢ \neg R \in V \to \underset{˙}{\cdot} = +_{M}$
17	9 16	pm2.61i	$⊢ \underset{˙}{\cdot} = +_{M}$

Metamath Proof Explorer