Theorem mgpplusg 18693

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

Hypotheses

Ref	Expression
mgpval.1	⊢ 𝑀 = (mulGrp‘𝑅)
mgpval.2	⊢ · = (.r‘𝑅)

Assertion

Ref	Expression
mgpplusg	⊢ · = (+g‘𝑀)

Proof of Theorem mgpplusg

Step	Hyp	Ref	Expression
1		mgpval.2	. . . . 5 ⊢ · = (.r‘𝑅)
2		fvex 6362	. . . . 5 ⊢ (.r‘𝑅) ∈ V
3	1, 2	eqeltri 2835	. . . 4 ⊢ · ∈ V
4		plusgid 16179	. . . . 5 ⊢ +g = Slot (+g‘ndx)
5	4	setsid 16116	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6	3, 5	mpan2 709	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
7		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
8	7, 1	mgpval 18692	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
9	8	fveq2i 6355	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
10	6, 9	syl6eqr 2812	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
11	4	str0 16113	. . 3 ⊢ ∅ = (+g‘∅)
12		fvprc 6346	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
13	1, 12	syl5eq 2806	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
14		fvprc 6346	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
15	7, 14	syl5eq 2806	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
16	15	fveq2d 6356	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
17	11, 13, 16	3eqtr4a 2820	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
18	10, 17	pm2.61i 176	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1632   ∈ wcel 2139  Vcvv 3340  ∅c0 4058  ⟨cop 4327  ‘cfv 6049  (class class class)co 6813  ndxcnx 16056   sSet csts 16057  +_gcplusg 16143  ._rcmulr 16144  mulGrpcmgp 18689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-i2m1 10196  ax-1ne0 10197  ax-rrecex 10200  ax-cnre 10201

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-nn 11213  df-2 11271  df-ndx 16062  df-slot 16063  df-sets 16066  df-plusg 16156  df-mgp 18690

This theorem is referenced by:  dfur2  18704  srgcl  18712  srgass  18713  srgideu  18714  srgidmlem  18720  issrgid  18723  srg1zr  18729  srgpcomp  18732  srgpcompp  18733  srgbinomlem4  18743  srgbinomlem  18744  csrgbinom  18746  ringcl  18761  crngcom  18762  iscrng2  18763  ringass  18764  ringideu  18765  ringidmlem  18770  isringid  18773  ringidss  18777  ringpropd  18782  crngpropd  18783  isringd  18785  iscrngd  18786  ring1  18802  gsummgp0  18808  prdsmgp  18810  oppr1  18834  unitgrp  18867  unitlinv  18877  unitrinv  18878  rngidpropd  18895  invrpropd  18898  dfrhm2  18919  rhmmul  18929  isrhm2d  18930  isdrng2  18959  drngmcl  18962  drngid2  18965  isdrngd  18974  subrgugrp  19001  issubrg3  19010  cntzsubr  19014  rhmpropd  19017  rlmscaf  19410  sraassa  19527  assamulgscmlem2  19551  psrcrng  19615  mplcoe3  19668  mplcoe5lem  19669  mplcoe5  19670  mplcoe2  19671  mplbas2  19672  evlslem1  19717  mpfind  19738  coe1tm  19845  ply1coe  19868  xrsmcmn  19971  cnfldexp  19981  cnmsubglem  20011  expmhm  20017  nn0srg  20018  rge0srg  20019  expghm  20046  psgnghm  20128  psgnco  20131  evpmodpmf1o  20144  ringvcl  20406  mamuvs2  20414  mat1mhm  20492  scmatmhm  20542  mdetdiaglem  20606  mdetrlin  20610  mdetrsca  20611  mdetralt  20616  mdetunilem7  20626  mdetuni0  20629  m2detleib  20639  invrvald  20684  mat2pmatmhm  20740  pm2mpmhm  20827  chfacfpmmulgsum2  20872  cpmadugsumlemB  20881  cnmpt1mulr  22186  cnmpt2mulr  22187  reefgim  24403  efabl  24495  efsubm  24496  amgm  24916  wilthlem2  24994  wilthlem3  24995  dchrelbas3  25162  dchrzrhmul  25170  dchrmulcl  25173  dchrn0  25174  dchrinvcl  25177  dchrptlem2  25189  dchrsum2  25192  sum2dchr  25198  lgseisenlem3  25301  lgseisenlem4  25302  rdivmuldivd  30100  ringinvval  30101  dvrcan5  30102  rhmunitinv  30131  iistmd  30257  xrge0iifmhm  30294  xrge0pluscn  30295  pl1cn  30310  cntzsdrg  38274  isdomn3  38284  mon1psubm  38286  deg1mhm  38287  amgm2d  39003  amgm3d  39004  amgm4d  39005  isringrng  42391  rngcl  42393  isrnghmmul  42403  lidlmmgm  42435  lidlmsgrp  42436  2zrngmmgm  42456  2zrngmsgrp  42457  2zrngnring  42462  cznrng  42465  cznnring  42466  mgpsumunsn  42650  invginvrid  42658  amgmlemALT  43062  amgmw2d  43063