Theorem mgpval

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

	Ref	Expression
Hypotheses	mgpval.1	$$⊢M={\mathrm{mulGrp}}_R$$
	mgpval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	mgpval	$$⊢M=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$

Proof

Step	Hyp	Ref	Expression
1		mgpval.1	$$⊢M={\mathrm{mulGrp}}_R$$
2		mgpval.2	$$⊢\underset{\dot{}}{·}={\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{\dot{}}{·}$$
6	5	opeq2d	$$⊢r=R\to ⟨{+}_{\mathrm{ndx}},{\cdot }_r⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
7	3 6	oveq12d	$$⊢r=R\to r\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_r⟩=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
8		df-mgp	$$⊢\mathrm{mulGrp}=\left(r\in \mathrm{V}⟼r\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_r⟩\right)$$
9		ovex	$$⊢R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢R\in \mathrm{V}\to {\mathrm{mulGrp}}_R=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
11		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{mulGrp}}_R=\varnothing$$
12		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
13	12	ovprc1	$$⊢\neg R\in \mathrm{V}\to R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩=\varnothing$$
14	11 13	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{mulGrp}}_R=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
15	10 14	pm2.61i	$$⊢{\mathrm{mulGrp}}_R=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
16	1 15	eqtri	$$⊢M=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$