Theorem mgpbasg 13884

Description: Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)

Hypotheses

Ref	Expression
mgpbas.1	|- M = (mulGrp ` R )
mgpbas.2	|- B = ( Base ` R )

Assertion

Ref	Expression
mgpbasg	|- ( R e. V -> B = ( Base ` M ) )

Proof of Theorem mgpbasg

Step	Hyp	Ref	Expression
1		mgpbas.2	. 2 |- B = ( Base ` R )
2		mulrslid 13160	. . . . 5 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
3	2	slotex 13054	. . . 4 |- ( R e. V -> ( .r ` R ) e. _V )
4		baseslid 13085	. . . . 5 |- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
5		basendxnplusgndx 13153	. . . . 5 |- ( Base ` ndx ) =/= ( +g ` ndx )
6		plusgslid 13140	. . . . . 6 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
7	6	simpri 113	. . . . 5 |- ( +g ` ndx ) e. NN
8	4, 5, 7	setsslnid 13079	. . . 4 |- ( ( R e. V /\ ( .r ` R ) e. _V ) -> ( Base ` R ) = ( Base ` ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) ) )
9	3, 8	mpdan 421	. . 3 |- ( R e. V -> ( Base ` R ) = ( Base ` ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) ) )
10		mgpbas.1	. . . . 5 |- M = (mulGrp ` R )
11		eqid 2229	. . . . 5 |- ( .r ` R ) = ( .r ` R )
12	10, 11	mgpvalg 13881	. . . 4 |- ( R e. V -> M = ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
13	12	fveq2d 5630	. . 3 |- ( R e. V -> ( Base ` M ) = ( Base ` ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) ) )
14	9, 13	eqtr4d 2265	. 2 |- ( R e. V -> ( Base ` R ) = ( Base ` M ) )
15	1, 14	eqtrid 2274	1 |- ( R e. V -> B = ( Base ` M ) )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   _Vcvv 2799   <.cop 3669   ` cfv 5317  (class class class)co 6000   NNcn 9106   ndxcnx 13024   sSet csts 13025  Slot cslot 13026   Basecbs 13027   +g cplusg 13105   .rcmulr 13106  mulGrpcmgp 13878

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 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-i2m1 8100  ax-0lt1 8101  ax-0id 8103  ax-rnegex 8104  ax-pre-ltirr 8107  ax-pre-ltadd 8111

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-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-iota 5277  df-fun 5319  df-fn 5320  df-fv 5325  df-ov 6003  df-oprab 6004  df-mpo 6005  df-pnf 8179  df-mnf 8180  df-ltxr 8182  df-inn 9107  df-2 9165  df-3 9166  df-ndx 13030  df-slot 13031  df-base 13033  df-sets 13034  df-plusg 13118  df-mulr 13119  df-mgp 13879

This theorem is referenced by:  mgptopng  13887  mgpress  13889  rngass  13897  rngcl  13902  isrngd  13911  rngpropd  13913  dfur2g  13920  srgcl  13928  srgass  13929  srgideu  13930  srgidcl  13934  srgidmlem  13936  issrgid  13939  srg1zr  13945  srgpcomp  13948  srgpcompp  13949  srgpcomppsc  13950  ringcl  13971  crngcom  13972  iscrng2  13973  ringass  13974  ringideu  13975  ringidcl  13978  ringidmlem  13980  isringid  13983  ringidss  13987  ringpropd  13996  crngpropd  13997  isringd  13999  iscrngd  14000  ring1  14017  oppr1g  14040  unitgrpbasd  14073  unitsubm  14077  rngidpropdg  14104  dfrhm2  14112  rhmmul  14122  isrhm2d  14123  rhmf1o  14126  subrgsubm  14192  issubrg3  14205  rhmpropd  14212  rnglidlmmgm  14454  rnglidlmsgrp  14455  cnfldexp  14535  expghmap  14565  lgseisenlem3  15745  lgseisenlem4  15746