Theorem mgpplusgg 13924

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

Hypotheses

Ref	Expression
mgpval.1	|- M = (mulGrp ` R )
mgpval.2	|- .x. = ( .r ` R )

Assertion

Ref	Expression
mgpplusgg	|- ( R e. V -> .x. = ( +g ` M ) )

Proof of Theorem mgpplusgg

Step	Hyp	Ref	Expression
1		mgpval.2	. . . 4 |- .x. = ( .r ` R )
2		mulrslid 13202	. . . . 5 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
3	2	slotex 13096	. . . 4 |- ( R e. V -> ( .r ` R ) e. _V )
4	1, 3	eqeltrid 2316	. . 3 |- ( R e. V -> .x. e. _V )
5		plusgslid 13182	. . . 4 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
6	5	setsslid 13120	. . 3 |- ( ( R e. V /\ .x. e. _V ) -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) )
7	4, 6	mpdan 421	. 2 |- ( R e. V -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) )
8		mgpval.1	. . . 4 |- M = (mulGrp ` R )
9	8, 1	mgpvalg 13923	. . 3 |- ( R e. V -> M = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
10	9	fveq2d 5637	. 2 |- ( R e. V -> ( +g ` M ) = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) )
11	7, 10	eqtr4d 2265	1 |- ( R e. V -> .x. = ( +g ` M ) )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   _Vcvv 2800   <.cop 3670   ` cfv 5322  (class class class)co 6011   ndxcnx 13066   sSet csts 13067   +g cplusg 13147   .rcmulr 13148  mulGrpcmgp 13920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295  ax-un 4526  ax-setind 4631  ax-cnex 8111  ax-resscn 8112  ax-1re 8114  ax-addrcl 8117

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-int 3925  df-br 4085  df-opab 4147  df-mpt 4148  df-id 4386  df-xp 4727  df-rel 4728  df-cnv 4729  df-co 4730  df-dm 4731  df-rn 4732  df-res 4733  df-iota 5282  df-fun 5324  df-fn 5325  df-fv 5330  df-ov 6014  df-oprab 6015  df-mpo 6016  df-inn 9132  df-2 9190  df-3 9191  df-ndx 13072  df-slot 13073  df-sets 13076  df-plusg 13160  df-mulr 13161  df-mgp 13921

This theorem is referenced by:  rngass  13939  rngcl  13944  isrngd  13953  rngpropd  13955  dfur2g  13962  srgcl  13970  srgass  13971  srgideu  13972  srgidmlem  13978  issrgid  13981  srg1zr  13987  srgpcomp  13990  srgpcompp  13991  ringcl  14013  crngcom  14014  iscrng2  14015  ringass  14016  ringideu  14017  ringidmlem  14022  isringid  14025  ringidss  14029  ringpropd  14038  crngpropd  14039  isringd  14041  iscrngd  14042  ring1  14059  oppr1g  14082  unitgrp  14117  unitlinv  14127  unitrinv  14128  rdivmuldivd  14145  rngidpropdg  14147  invrpropdg  14150  dfrhm2  14155  rhmmul  14165  isrhm2d  14166  rhmunitinv  14179  subrgugrp  14241  issubrg3  14248  rhmpropd  14255  rnglidlmmgm  14497  rnglidlmsgrp  14498  cnfldexp  14578  expghmap  14608  lgseisenlem3  15788  lgseisenlem4  15789