![]() |
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 6559 | . . . 4 ⊢ · ∈ V |
3 | plusgid 16429 | . . . . 5 ⊢ +g = Slot (+g‘ndx) | |
4 | 3 | setsid 16371 | . . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉))) |
5 | 2, 4 | mpan2 687 | . . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉))) |
6 | mgpval.1 | . . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅) | |
7 | 6, 1 | mgpval 18936 | . . . 4 ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) |
8 | 7 | fveq2i 6548 | . . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet 〈(+g‘ndx), · 〉)) |
9 | 5, 8 | syl6eqr 2851 | . 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀)) |
10 | 3 | str0 16368 | . . 3 ⊢ ∅ = (+g‘∅) |
11 | fvprc 6538 | . . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅) | |
12 | 1, 11 | syl5eq 2845 | . . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅) |
13 | fvprc 6538 | . . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅) | |
14 | 6, 13 | syl5eq 2845 | . . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅) |
15 | 14 | fveq2d 6549 | . . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅)) |
16 | 10, 12, 15 | 3eqtr4a 2859 | . 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀)) |
17 | 9, 16 | pm2.61i 183 | 1 ⊢ · = (+g‘𝑀) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1525 ∈ wcel 2083 Vcvv 3440 ∅c0 4217 〈cop 4484 ‘cfv 6232 (class class class)co 7023 ndxcnx 16313 sSet csts 16314 +gcplusg 16398 .rcmulr 16399 mulGrpcmgp 18933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-1cn 10448 ax-addcl 10450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-nn 11493 df-2 11554 df-ndx 16319 df-slot 16320 df-sets 16323 df-plusg 16411 df-mgp 18934 |
This theorem is referenced by: dfur2 18948 srgcl 18956 srgass 18957 srgideu 18958 srgidmlem 18964 issrgid 18967 srg1zr 18973 srgpcomp 18976 srgpcompp 18977 srgbinomlem4 18987 srgbinomlem 18988 csrgbinom 18990 ringcl 19005 crngcom 19006 iscrng2 19007 ringass 19008 ringideu 19009 ringidmlem 19014 isringid 19017 ringidss 19021 ringpropd 19026 crngpropd 19027 isringd 19029 iscrngd 19030 ring1 19046 gsummgp0 19052 prdsmgp 19054 oppr1 19078 unitgrp 19111 unitlinv 19121 unitrinv 19122 rngidpropd 19139 invrpropd 19142 dfrhm2 19163 rhmmul 19173 isrhm2d 19174 isdrng2 19206 drngmcl 19209 drngid2 19212 isdrngd 19221 subrgugrp 19248 issubrg3 19257 cntzsubr 19262 rhmpropd 19265 cntzsdrg 19275 primefld 19278 rlmscaf 19674 sraassa 19791 assamulgscmlem2 19821 psrcrng 19885 mplcoe3 19938 mplcoe5lem 19939 mplcoe5 19940 mplcoe2 19941 mplbas2 19942 evlslem1 19986 mpfind 20007 coe1tm 20128 ply1coe 20151 xrsmcmn 20254 cnfldexp 20264 cnmsubglem 20294 expmhm 20300 nn0srg 20301 rge0srg 20302 expghm 20329 psgnghm 20410 psgnco 20413 evpmodpmf1o 20426 ringvcl 20695 mamuvs2 20703 mat1mhm 20781 scmatmhm 20831 mdetdiaglem 20895 mdetrlin 20899 mdetrsca 20900 mdetralt 20905 mdetunilem7 20915 mdetuni0 20918 m2detleib 20928 invrvald 20973 mat2pmatmhm 21029 pm2mpmhm 21116 chfacfpmmulgsum2 21161 cpmadugsumlemB 21170 cnmpt1mulr 22477 cnmpt2mulr 22478 reefgim 24725 efabl 24819 efsubm 24820 amgm 25254 wilthlem2 25332 wilthlem3 25333 dchrelbas3 25500 dchrzrhmul 25508 dchrmulcl 25511 dchrn0 25512 dchrinvcl 25515 dchrptlem2 25527 dchrsum2 25530 sum2dchr 25536 lgseisenlem3 25639 lgseisenlem4 25640 rdivmuldivd 30512 ringinvval 30513 dvrcan5 30514 rhmunitinv 30545 iistmd 30758 xrge0iifmhm 30795 xrge0pluscn 30796 pl1cn 30811 isdomn3 39310 mon1psubm 39312 deg1mhm 39313 amgm2d 40058 amgm3d 40059 amgm4d 40060 isringrng 43652 rngcl 43654 isrnghmmul 43664 lidlmmgm 43696 lidlmsgrp 43697 2zrngmmgm 43717 2zrngmsgrp 43718 2zrngnring 43723 cznrng 43726 cznnring 43727 mgpsumunsn 43909 invginvrid 43917 amgmlemALT 44406 amgmw2d 44407 |
Copyright terms: Public domain | W3C validator |