mgpval

Description: Value of the multiplication group operation. (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		id	$⊢ r = R \to r = R$
4		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
5	4 2	eqtr4di	$⊢ r = R \to \cdot_{r} = \underset{˙}{\cdot}$
6	5	opeq2d	$⊢ r = R \to ⟨+_{ndx}, \cdot_{r}⟩ = ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
7	3 6	oveq12d	$⊢ r = R \to r sSet ⟨+_{ndx}, \cdot_{r}⟩ = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
8		df-mgp	$⊢ mulGrp = (r \in V ⟼ r sSet ⟨+_{ndx}, \cdot_{r}⟩)$
9		ovex	$⊢ R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩ \in V$
10	7 8 9	fvmpt	$⊢ R \in V \to {mulGrp}_{R} = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
11		fvprc	$⊢ \neg R \in V \to {mulGrp}_{R} = \emptyset$
12		reldmsets	$⊢ Rel dom sSet$
13	12	ovprc1	$⊢ \neg R \in V \to R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩ = \emptyset$
14	11 13	eqtr4d	$⊢ \neg R \in V \to {mulGrp}_{R} = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
15	10 14	pm2.61i	$⊢ {mulGrp}_{R} = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$
16	1 15	eqtri	$⊢ M = R sSet ⟨+_{ndx}, \underset{˙}{\cdot}⟩$

Metamath Proof Explorer