![]() |
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 6860 | . . . 4 β’ Β· β V |
3 | plusgid 17168 | . . . . 5 β’ +g = Slot (+gβndx) | |
4 | 3 | setsid 17088 | . . . 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 19907 | . . . 4 β’ π = (π sSet β¨(+gβndx), Β· β©) |
8 | 7 | fveq2i 6849 | . . 3 β’ (+gβπ) = (+gβ(π sSet β¨(+gβndx), Β· β©)) |
9 | 5, 8 | eqtr4di 2791 | . 2 β’ (π β V β Β· = (+gβπ)) |
10 | 3 | str0 17069 | . . 3 β’ β = (+gββ ) |
11 | fvprc 6838 | . . . 4 β’ (Β¬ π β V β (.rβπ ) = β ) | |
12 | 1, 11 | eqtrid 2785 | . . 3 β’ (Β¬ π β V β Β· = β ) |
13 | fvprc 6838 | . . . . 5 β’ (Β¬ π β V β (mulGrpβπ ) = β ) | |
14 | 6, 13 | eqtrid 2785 | . . . 4 β’ (Β¬ π β V β π = β ) |
15 | 14 | fveq2d 6850 | . . 3 β’ (Β¬ π β V β (+gβπ) = (+gββ )) |
16 | 10, 12, 15 | 3eqtr4a 2799 | . 2 β’ (Β¬ π β V β Β· = (+gβπ)) |
17 | 9, 16 | pm2.61i 182 | 1 β’ Β· = (+gβπ) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 = wceq 1542 β wcel 2107 Vcvv 3447 β c0 4286 β¨cop 4596 βcfv 6500 (class class class)co 7361 sSet csts 17043 ndxcnx 17073 +gcplusg 17141 .rcmulr 17142 mulGrpcmgp 19904 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pow 5324 ax-pr 5388 ax-un 7676 ax-cnex 11115 ax-1cn 11117 ax-addcl 11119 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3933 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-iun 4960 df-br 5110 df-opab 5172 df-mpt 5193 df-tr 5227 df-id 5535 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5592 df-we 5594 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-pred 6257 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-iota 6452 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7807 df-2nd 7926 df-frecs 8216 df-wrecs 8247 df-recs 8321 df-rdg 8360 df-nn 12162 df-2 12224 df-sets 17044 df-slot 17062 df-ndx 17074 df-plusg 17154 df-mgp 19905 |
This theorem is referenced by: dfur2 19924 srgcl 19932 srgass 19933 srgideu 19934 srgidmlem 19940 issrgid 19943 srg1zr 19954 srgpcomp 19957 srgpcompp 19958 srgbinomlem4 19968 srgbinomlem 19969 csrgbinom 19971 ringcl 19989 crngcom 19990 iscrng2 19991 ringass 19992 ringideu 19993 ringidmlem 19999 isringid 20002 ringidss 20006 ringpropd 20014 crngpropd 20015 isringd 20017 iscrngd 20018 ring1 20034 gsummgp0 20040 prdsmgp 20042 pwspjmhmmgpd 20051 oppr1 20071 unitgrp 20104 unitlinv 20114 unitrinv 20115 rdivmuldivd 20132 rngidpropd 20134 invrpropd 20137 dfrhm2 20158 rhmmul 20169 isrhm2d 20170 rhmunitinv 20194 isdrng2 20232 drngmcl 20235 drngid2 20239 isdrngd 20249 isdrngdOLD 20251 subrgugrp 20283 issubrg3 20293 cntzsubr 20298 rhmpropd 20301 cntzsdrg 20312 primefld 20315 rlmscaf 20723 xrsmcmn 20843 cnfldexp 20853 cnmsubglem 20883 expmhm 20889 nn0srg 20890 rge0srg 20891 expghm 20919 psgnghm 21007 psgnco 21010 evpmodpmf1o 21023 sraassa 21296 assamulgscmlem2 21326 psrcrng 21405 mplcoe3 21462 mplcoe5lem 21463 mplcoe5 21464 mplcoe2 21465 mplbas2 21466 evlslem1 21515 mpfind 21540 mhppwdeg 21563 coe1tm 21667 ply1coe 21690 ringvcl 21770 mamuvs2 21776 mat1mhm 21856 scmatmhm 21906 mdetdiaglem 21970 mdetrlin 21974 mdetrsca 21975 mdetralt 21980 mdetunilem7 21990 mdetuni0 21993 m2detleib 22003 invrvald 22048 mat2pmatmhm 22105 pm2mpmhm 22192 chfacfpmmulgsum2 22237 cpmadugsumlemB 22246 cnmpt1mulr 23556 cnmpt2mulr 23557 reefgim 25832 efabl 25929 efsubm 25930 amgm 26363 wilthlem2 26441 wilthlem3 26442 dchrelbas3 26609 dchrzrhmul 26617 dchrmulcl 26620 dchrn0 26621 dchrinvcl 26624 dchrptlem2 26636 dchrsum2 26639 sum2dchr 26645 lgseisenlem3 26748 lgseisenlem4 26749 frobrhm 32124 ringinvval 32126 dvrcan5 32127 elringlsm 32229 lsmsnpridl 32234 cringm4 32274 mxidlprm 32292 iistmd 32547 xrge0iifmhm 32584 xrge0pluscn 32585 pl1cn 32600 mhphf 40818 isdomn3 41578 mon1psubm 41580 deg1mhm 41581 amgm2d 42563 amgm3d 42564 amgm4d 42565 isringrng 46269 rngcl 46271 isrnghmmul 46281 lidlmmgm 46313 lidlmsgrp 46314 2zrngmmgm 46334 2zrngmsgrp 46335 2zrngnring 46340 cznrng 46343 cznnring 46344 mgpsumunsn 46527 invginvrid 46533 amgmlemALT 47340 amgmw2d 47341 |
Copyright terms: Public domain | W3C validator |