Theorem mgpplusg

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

	Ref	Expression
Hypotheses	mgpval.1	$$⊢M={\mathrm{mulGrp}}_R$$
	mgpval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_M$$

Proof

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