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 = ( mulGrp ` R )
	mgpval.2	|- .x. = ( .r ` R )
Assertion	mgpplusg	|- .x. = ( +g ` M )

Proof

Step	Hyp	Ref	Expression
1		mgpval.1	|- M = ( mulGrp ` R )
2		mgpval.2	|- .x. = ( .r ` R )
3	2	fvexi	|- .x. e. _V
4		plusgid	|- +g = Slot ( +g ` ndx )
5	4	setsid	|- ( ( R e. _V /\ .x. e. _V ) -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) )
6	3 5	mpan2	|- ( R e. _V -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) )
7	1 2	mgpval	|- M = ( R sSet <. ( +g ` ndx ) , .x. >. )
8	7	fveq2i	|- ( +g ` M ) = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) )
9	6 8	eqtr4di	|- ( R e. _V -> .x. = ( +g ` M ) )
10	4	str0	|- (/) = ( +g ` (/) )
11		fvprc	|- ( -. R e. _V -> ( .r ` R ) = (/) )
12	2 11	syl5eq	|- ( -. R e. _V -> .x. = (/) )
13		fvprc	|- ( -. R e. _V -> ( mulGrp ` R ) = (/) )
14	1 13	syl5eq	|- ( -. R e. _V -> M = (/) )
15	14	fveq2d	|- ( -. R e. _V -> ( +g ` M ) = ( +g ` (/) ) )
16	10 12 15	3eqtr4a	|- ( -. R e. _V -> .x. = ( +g ` M ) )
17	9 16	pm2.61i	|- .x. = ( +g ` M )