Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprdval Structured version   Unicode version

Theorem dprdval 16884
 Description: The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
Hypotheses
Ref Expression
dprdval.0
dprdval.w finSupp
Assertion
Ref Expression
dprdval DProd DProd g
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem dprdval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 457 . 2 DProd DProd
2 reldmdprd 16878 . . . . . 6 DProd
32brrelex2i 5046 . . . . 5 DProd
43adantr 465 . . . 4 DProd
52brrelexi 5045 . . . . . 6 DProd
6 breq1 4455 . . . . . . . 8 DProd DProd
7 oveq1 6301 . . . . . . . . 9 DProd DProd
8 fveq2 5871 . . . . . . . . . . . . . 14
9 dprdval.0 . . . . . . . . . . . . . 14
108, 9syl6eqr 2526 . . . . . . . . . . . . 13
1110breq2d 4464 . . . . . . . . . . . 12 finSupp finSupp
1211rabbidv 3110 . . . . . . . . . . 11 finSupp finSupp
13 oveq1 6301 . . . . . . . . . . 11 g g
1412, 13mpteq12dv 4530 . . . . . . . . . 10 finSupp g finSupp g
1514rneqd 5235 . . . . . . . . 9 finSupp g finSupp g
167, 15eqeq12d 2489 . . . . . . . 8 DProd finSupp g DProd finSupp g
176, 16imbi12d 320 . . . . . . 7 DProd DProd finSupp g DProd DProd finSupp g
18 df-br 4453 . . . . . . . . 9 DProd DProd
19 fvex 5881 . . . . . . . . . . . . . . . . . 18
2019rgenw 2828 . . . . . . . . . . . . . . . . 17
21 ixpexg 7503 . . . . . . . . . . . . . . . . 17
2220, 21ax-mp 5 . . . . . . . . . . . . . . . 16
2322rabex 4603 . . . . . . . . . . . . . . 15 finSupp
2423mptex 6141 . . . . . . . . . . . . . 14 finSupp g
2524rnex 6728 . . . . . . . . . . . . 13 finSupp g
2625rgen2w 2829 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp finSupp g
27 df-dprd 16876 . . . . . . . . . . . . 13 DProd SubGrp Cntz mrClsSubGrp finSupp g
2827fmpt2x 6860 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp finSupp g DProd SubGrp Cntz mrClsSubGrp
2926, 28mpbi 208 . . . . . . . . . . 11 DProd SubGrp Cntz mrClsSubGrp
3029fdmi 5741 . . . . . . . . . 10 DProd SubGrp Cntz mrClsSubGrp
3130eleq2i 2545 . . . . . . . . 9 DProd SubGrp Cntz mrClsSubGrp
32 opeliunxp 5056 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp SubGrp Cntz mrClsSubGrp
3318, 31, 323bitri 271 . . . . . . . 8 DProd SubGrp Cntz mrClsSubGrp
3427ovmpt4g 6419 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp finSupp g DProd finSupp g
3525, 34mp3an3 1313 . . . . . . . 8 SubGrp Cntz mrClsSubGrp DProd finSupp g
3633, 35sylbi 195 . . . . . . 7 DProd DProd finSupp g
3717, 36vtoclg 3176 . . . . . 6 DProd DProd finSupp g
385, 37mpcom 36 . . . . 5 DProd DProd finSupp g
3938sbcth 3351 . . . 4 DProd DProd finSupp g
404, 39syl 16 . . 3 DProd DProd DProd finSupp g
41 simpr 461 . . . . . 6 DProd
4241breq2d 4464 . . . . 5 DProd DProd DProd
4341oveq2d 6310 . . . . . 6 DProd DProd DProd
4441dmeqd 5210 . . . . . . . . . . . . 13 DProd
45 simplr 754 . . . . . . . . . . . . 13 DProd
4644, 45eqtrd 2508 . . . . . . . . . . . 12 DProd
4746ixpeq1d 7491 . . . . . . . . . . 11 DProd
4841fveq1d 5873 . . . . . . . . . . . 12 DProd
4948ixpeq2dv 7495 . . . . . . . . . . 11 DProd
5047, 49eqtrd 2508 . . . . . . . . . 10 DProd
51 biidd 237 . . . . . . . . . 10 DProd finSupp finSupp
5250, 51rabeqbidv 3113 . . . . . . . . 9 DProd finSupp finSupp
53 dprdval.w . . . . . . . . 9 finSupp
5452, 53syl6eqr 2526 . . . . . . . 8 DProd finSupp
55 eqidd 2468 . . . . . . . 8 DProd g g
5654, 55mpteq12dv 4530 . . . . . . 7 DProd finSupp g g
5756rneqd 5235 . . . . . 6 DProd finSupp g g
5843, 57eqeq12d 2489 . . . . 5 DProd DProd finSupp g DProd g
5942, 58imbi12d 320 . . . 4 DProd DProd DProd finSupp g DProd DProd g
604, 59sbcied 3373 . . 3 DProd DProd DProd finSupp g DProd DProd g
6140, 60mpbid 210 . 2 DProd DProd DProd g
621, 61mpd 15 1 DProd DProd g
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767  cab 2452  wral 2817  crab 2821  cvv 3118  wsbc 3336   cdif 3478   cin 3480   wss 3481  csn 4032  cop 4038  cuni 4250  ciun 4330   class class class wbr 4452   cmpt 4510   cxp 5002   cdm 5004   crn 5005  cima 5007  wf 5589  cfv 5593  (class class class)co 6294  cixp 7479   finSupp cfsupp 7839  c0g 14707   g cgsu 14708  mrClscmrc 14850  cgrp 15902  SubGrpcsubg 16044  Cntzccntz 16202   DProd cdprd 16874 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6297  df-oprab 6298  df-mpt2 6299  df-1st 6794  df-2nd 6795  df-ixp 7480  df-dprd 16876 This theorem is referenced by:  eldprd  16885  dprdlub  16922
 Copyright terms: Public domain W3C validator