![]() |
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 | 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‘𝑀) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |