![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mgpplusg | Structured version Visualization version GIF version |
Description: Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
Ref | Expression |
---|---|
mgpval.1 | ⊢ 𝑀 = (mulGrp‘𝑅) |
mgpval.2 | ⊢ · = (.r‘𝑅) |
Ref | Expression |
---|---|
mgpplusg | ⊢ · = (+g‘𝑀) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgpval.2 | . . . . 5 ⊢ · = (.r‘𝑅) | |
2 | 1 | fvexi 6905 | . . . 4 ⊢ · ∈ V |
3 | plusgid 17251 | . . . . 5 ⊢ +g = Slot (+g‘ndx) | |
4 | 3 | setsid 17168 | . . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉))) |
5 | 2, 4 | mpan2 690 | . . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉))) |
6 | mgpval.1 | . . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅) | |
7 | 6, 1 | mgpval 20068 | . . . 4 ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) |
8 | 7 | fveq2i 6894 | . . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉)) |
9 | 5, 8 | eqtr4di 2785 | . 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀)) |
10 | 3 | str0 17149 | . . 3 ⊢ ∅ = (+g‘∅) |
11 | fvprc 6883 | . . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅) | |
12 | 1, 11 | eqtrid 2779 | . . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅) |
13 | fvprc 6883 | . . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅) | |
14 | 6, 13 | eqtrid 2779 | . . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅) |
15 | 14 | fveq2d 6895 | . . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅)) |
16 | 10, 12, 15 | 3eqtr4a 2793 | . 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀)) |
17 | 9, 16 | pm2.61i 182 | 1 ⊢ · = (+g‘𝑀) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1534 ∈ wcel 2099 Vcvv 3469 ∅c0 4318 〈cop 4630 ‘cfv 6542 (class class class)co 7414 sSet csts 17123 ndxcnx 17153 +gcplusg 17224 .rcmulr 17225 mulGrpcmgp 20065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-1cn 11188 ax-addcl 11190 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-ral 3057 df-rex 3066 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-nn 12235 df-2 12297 df-sets 17124 df-slot 17142 df-ndx 17154 df-plusg 17237 df-mgp 20066 |
This theorem is referenced by: prdsmgp 20082 rngass 20090 rngcl 20095 isrngd 20104 rngpropd 20105 dfur2 20115 srgcl 20124 srgass 20125 srgideu 20126 srgidmlem 20132 issrgid 20135 srg1zr 20146 srgpcomp 20149 srgpcompp 20150 srgbinomlem4 20160 srgbinomlem 20161 csrgbinom 20163 ringcl 20181 crngcom 20182 iscrng2 20183 ringass 20184 ringideu 20185 ringidmlem 20193 isringid 20196 ringidss 20202 isringrng 20212 ringpropd 20213 crngpropd 20214 isringd 20216 iscrngd 20217 ring1 20235 gsummgp0 20243 pwspjmhmmgpd 20253 xpsring1d 20258 oppr1 20278 unitgrp 20311 unitlinv 20321 unitrinv 20322 rdivmuldivd 20341 rngidpropd 20343 invrpropd 20346 isrnghmmul 20370 dfrhm2 20402 rhmmul 20414 isrhm2d 20415 rhmunitinv 20439 rhmimasubrnglem 20491 rhmimasubrng 20492 cntzsubrng 20493 subrgugrp 20519 issubrg3 20528 cntzsubr 20534 rhmpropd 20537 isdrng2 20627 drngmcl 20630 drngid2 20634 isdrngd 20646 isdrngdOLD 20648 cntzsdrg 20679 primefld 20682 rlmscaf 21089 rnglidlmmgm 21129 rnglidlmsgrp 21130 rng2idl1cntr 21184 xrsmcmn 21306 cnfldexp 21319 cnmsubglem 21350 expmhm 21356 nn0srg 21357 rge0srg 21358 expghm 21388 psgnghm 21499 psgnco 21502 evpmodpmf1o 21515 sraassab 21788 sraassaOLD 21790 assamulgscmlem2 21820 psrcrng 21902 mplcoe3 21963 mplcoe5lem 21964 mplcoe5 21965 mplcoe2 21966 mplbas2 21967 evlslem1 22015 mpfind 22040 mhppwdeg 22061 coe1tm 22179 ply1coe 22204 ringvcl 22287 mamuvs2 22293 mat1mhm 22373 scmatmhm 22423 mdetdiaglem 22487 mdetrlin 22491 mdetrsca 22492 mdetralt 22497 mdetunilem7 22507 mdetuni0 22510 m2detleib 22520 invrvald 22565 mat2pmatmhm 22622 pm2mpmhm 22709 chfacfpmmulgsum2 22754 cpmadugsumlemB 22763 cnmpt1mulr 24073 cnmpt2mulr 24074 reefgim 26374 efabl 26471 efsubm 26472 amgm 26910 wilthlem2 26988 wilthlem3 26989 dchrelbas3 27158 dchrzrhmul 27166 dchrmulcl 27169 dchrn0 27170 dchrinvcl 27173 dchrptlem2 27185 dchrsum2 27188 sum2dchr 27194 lgseisenlem3 27297 lgseisenlem4 27298 urpropd 32916 frobrhm 32918 ringinvval 32920 dvrcan5 32921 elringlsm 33042 lsmsnpridl 33047 cringm4 33098 mxidlprm 33119 evls1fldgencl 33290 iistmd 33439 xrge0iifmhm 33476 xrge0pluscn 33477 pl1cn 33492 aks6d1c1p4 41515 evl1gprodd 41521 idomnnzpownz 41535 idomnnzgmulnz 41536 ringexp0nn 41537 aks6d1c5lem3 41540 aks6d1c5lem2 41541 deg1gprod 41544 deg1pow 41545 selvvvval 41740 evlselv 41742 mhphf 41752 isdomn3 42549 mon1psubm 42550 deg1mhm 42551 amgm2d 43551 amgm3d 43552 amgm4d 43553 2zrngmmgm 47237 2zrngmsgrp 47238 2zrngnring 47243 cznrng 47246 cznnring 47247 mgpsumunsn 47348 invginvrid 47354 amgmlemALT 48159 amgmw2d 48160 |
Copyright terms: Public domain | W3C validator |