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

Theorem dpjidclOLD 17434
 Description: The key property of projections: the sum of all the projections of is . (Contributed by Mario Carneiro, 26-Apr-2016.) Obsolete version of dpjidcl 17427 as of 14-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
dpjidclOLD.1 DProd
dpjidclOLD.2
dpjidclOLD.p dProj
dpjidclOLD.3 DProd
dpjidclOLD.0
dpjidclOLD.w
Assertion
Ref Expression
dpjidclOLD g
Distinct variable groups:   ,,   ,,,   ,,   ,,   ,,,   ,   ,,   ,,,
Allowed substitution hints:   ()   ()   ()   (,)   ()

Proof of Theorem dpjidclOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dpjidclOLD.3 . . . 4 DProd
2 dpjidclOLD.2 . . . . 5
3 dpjidclOLD.0 . . . . . 6
4 dpjidclOLD.w . . . . . 6
53, 4eldprdOLD 17357 . . . . 5 DProd DProd g
62, 5syl 17 . . . 4 DProd DProd g
71, 6mpbid 210 . . 3 DProd g
87simprd 461 . 2 g
9 dpjidclOLD.1 . . . . 5 DProd
109adantr 463 . . . 4 g DProd
112adantr 463 . . . 4 g
129ad2antrr 724 . . . . . 6 g DProd
132ad2antrr 724 . . . . . 6 g
14 dpjidclOLD.p . . . . . 6 dProj
15 simpr 459 . . . . . 6 g
1612, 13, 14, 15dpjf 17426 . . . . 5 g DProd
171ad2antrr 724 . . . . 5 g DProd
1816, 17ffvelrnd 6010 . . . 4 g
19 simprl 756 . . . . . 6 g
204, 10, 11, 19dprdffiOLD 17374 . . . . 5 g
21 eldifi 3565 . . . . . . . 8
22 eqid 2402 . . . . . . . . . 10
2312, 13, 14, 22, 15dpjval 17425 . . . . . . . . 9 g DProd
2423fveq1d 5851 . . . . . . . 8 g DProd
2521, 24sylan2 472 . . . . . . 7 g DProd
26 simplrr 763 . . . . . . . . . 10 g g
27 eqid 2402 . . . . . . . . . . 11
28 eqid 2402 . . . . . . . . . . 11 Cntz Cntz
29 dprdgrp 17358 . . . . . . . . . . . . 13 DProd
30 grpmnd 16386 . . . . . . . . . . . . 13
3110, 29, 303syl 18 . . . . . . . . . . . 12 g
3231adantr 463 . . . . . . . . . . 11 g
33 reldmdprd 17348 . . . . . . . . . . . . . . 15 DProd
3433brrelex2i 4865 . . . . . . . . . . . . . 14 DProd
35 dmexg 6715 . . . . . . . . . . . . . 14
3610, 34, 353syl 18 . . . . . . . . . . . . 13 g
3711, 36eqeltrrd 2491 . . . . . . . . . . . 12 g
3837adantr 463 . . . . . . . . . . 11 g
394, 10, 11, 19, 27dprdffOLD 17372 . . . . . . . . . . . 12 g
4039adantr 463 . . . . . . . . . . 11 g
4119adantr 463 . . . . . . . . . . . . 13 g
424, 12, 13, 41, 28dprdfcntzOLD 17375 . . . . . . . . . . . 12 g Cntz
4321, 42sylan2 472 . . . . . . . . . . 11 g Cntz
44 snssi 4116 . . . . . . . . . . . . 13
4544adantl 464 . . . . . . . . . . . 12 g
4645difss2d 3573 . . . . . . . . . . . . 13 g
47 cnvimass 5177 . . . . . . . . . . . . . . 15
48 fdm 5718 . . . . . . . . . . . . . . . 16
4939, 48syl 17 . . . . . . . . . . . . . . 15 g
5047, 49syl5sseq 3490 . . . . . . . . . . . . . 14 g
5150adantr 463 . . . . . . . . . . . . 13 g
52 ssconb 3576 . . . . . . . . . . . . 13
5346, 51, 52syl2anc 659 . . . . . . . . . . . 12 g
5445, 53mpbid 210 . . . . . . . . . . 11 g
5520adantr 463 . . . . . . . . . . 11 g
5627, 3, 28, 32, 38, 40, 43, 54, 55gsumzresOLD 17242 . . . . . . . . . 10 g g g
5726, 56eqtr4d 2446 . . . . . . . . 9 g g
58 eqid 2402 . . . . . . . . . . 11
59 difss 3570 . . . . . . . . . . . . . 14
6059a1i 11 . . . . . . . . . . . . 13 g
6112, 13, 60dprdres 17395 . . . . . . . . . . . 12 g DProd DProd DProd
6261simpld 457 . . . . . . . . . . 11 g DProd
6312, 13dprdf2 17360 . . . . . . . . . . . . 13 g SubGrp
64 fssres 5734 . . . . . . . . . . . . 13 SubGrp SubGrp
6563, 59, 64sylancl 660 . . . . . . . . . . . 12 g SubGrp
66 fdm 5718 . . . . . . . . . . . 12 SubGrp
6765, 66syl 17 . . . . . . . . . . 11 g
6839adantr 463 . . . . . . . . . . . . . . 15 g
6968feqmptd 5902 . . . . . . . . . . . . . 14 g
7069reseq1d 5093 . . . . . . . . . . . . 13 g
71 resmpt 5143 . . . . . . . . . . . . . 14
7259, 71ax-mp 5 . . . . . . . . . . . . 13
7370, 72syl6eq 2459 . . . . . . . . . . . 12 g
74 eldifi 3565 . . . . . . . . . . . . . . 15
754, 12, 13, 41dprdfclOLD 17373 . . . . . . . . . . . . . . 15 g
7674, 75sylan2 472 . . . . . . . . . . . . . 14 g
77 fvres 5863 . . . . . . . . . . . . . . 15
7877adantl 464 . . . . . . . . . . . . . 14 g
7976, 78eleqtrrd 2493 . . . . . . . . . . . . 13 g
8020adantr 463 . . . . . . . . . . . . . 14 g
81 ssdif 3578 . . . . . . . . . . . . . . . . . 18
8259, 81ax-mp 5 . . . . . . . . . . . . . . . . 17
8382sseli 3438 . . . . . . . . . . . . . . . 16
84 ssid 3461 . . . . . . . . . . . . . . . . . 18
8584a1i 11 . . . . . . . . . . . . . . . . 17 g
8668, 85suppssrOLD 5999 . . . . . . . . . . . . . . . 16 g
8783, 86sylan2 472 . . . . . . . . . . . . . . 15 g
8887suppss2OLD 6511 . . . . . . . . . . . . . 14 g
89 ssfi 7775 . . . . . . . . . . . . . 14
9080, 88, 89syl2anc 659 . . . . . . . . . . . . 13 g
9158, 62, 67, 79, 90dprdwdOLD 17371 . . . . . . . . . . . 12 g
9273, 91eqeltrd 2490 . . . . . . . . . . 11 g
933, 58, 62, 67, 92eldprdiOLD 17385 . . . . . . . . . 10 g g DProd
9421, 93sylan2 472 . . . . . . . . 9 g g DProd
9557, 94eqeltrd 2490 . . . . . . . 8 g DProd
96 eqid 2402 . . . . . . . . . 10
97 eqid 2402 . . . . . . . . . 10
9863, 15ffvelrnd 6010 . . . . . . . . . 10 g SubGrp
99 dprdsubg 17391 . . . . . . . . . . 11 DProd DProd SubGrp
10062, 99syl 17 . . . . . . . . . 10 g DProd SubGrp
10112, 13, 15, 3dpjdisj 17422 . . . . . . . . . 10 g DProd
10212, 13, 15, 28dpjcntz 17421 . . . . . . . . . 10 g Cntz DProd
10396, 97, 3, 28, 98, 100, 101, 102, 22pj1rid 17044 . . . . . . . . 9 g DProd DProd
10421, 103sylanl2 649 . . . . . . . 8 g DProd DProd
10595, 104mpdan 666 . . . . . . 7 g DProd
10625, 105eqtrd 2443 . . . . . 6 g
107106suppss2OLD 6511 . . . . 5 g
108 ssfi 7775 . . . . 5
10920, 107, 108syl2anc 659 . . . 4 g
1104, 10, 11, 18, 109dprdwdOLD 17371 . . 3 g
111 simprr 758 . . . 4 g g
11239feqmptd 5902 . . . . . 6 g
113 simplrr 763 . . . . . . . . . . 11 g g
11412, 29, 303syl 18 . . . . . . . . . . . 12 g
11512, 34, 353syl 18 . . . . . . . . . . . . 13 g
11613, 115eqeltrrd 2491 . . . . . . . . . . . 12 g
1174, 12, 13, 41dprdffiOLD 17374 . . . . . . . . . . . 12 g
118 disjdif 3844 . . . . . . . . . . . . 13
119118a1i 11 . . . . . . . . . . . 12 g
120 undif2 3848 . . . . . . . . . . . . 13
12115snssd 4117 . . . . . . . . . . . . . 14 g
122 ssequn1 3613 . . . . . . . . . . . . . 14
123121, 122sylib 196 . . . . . . . . . . . . 13 g
124120, 123syl5req 2456 . . . . . . . . . . . 12 g
12527, 3, 96, 28, 114, 116, 68, 42, 117, 119, 124gsumzsplitOLD 17269 . . . . . . . . . . 11 g g g g
12668, 121feqresmpt 5903 . . . . . . . . . . . . . 14 g
127126oveq2d 6294 . . . . . . . . . . . . 13 g g g
12868, 15ffvelrnd 6010 . . . . . . . . . . . . . 14 g
129 fveq2 5849 . . . . . . . . . . . . . . 15
13027, 129gsumsn 17302 . . . . . . . . . . . . . 14 g
131114, 15, 128, 130syl3anc 1230 . . . . . . . . . . . . 13 g g
132127, 131eqtrd 2443 . . . . . . . . . . . 12 g g
133132oveq1d 6293 . . . . . . . . . . 11 g g g g
134113, 125, 1333eqtrd 2447 . . . . . . . . . 10 g g
13512, 13, 15, 97dpjlsm 17423 . . . . . . . . . . . 12 g DProd DProd
13617, 135eleqtrd 2492 . . . . . . . . . . 11 g DProd
1374, 10, 11, 19dprdfclOLD 17373 . . . . . . . . . . 11 g
13896, 97, 3, 28, 98, 100, 101, 102, 22, 136, 137, 93pj1eq 17042 . . . . . . . . . 10 g g DProd DProd g
139134, 138mpbid 210 . . . . . . . . 9 g DProd DProd g
140139simpld 457 . . . . . . . 8 g DProd
14124, 140eqtrd 2443 . . . . . . 7 g
142141mpteq2dva 4481 . . . . . 6 g
143112, 142eqtr4d 2446 . . . . 5 g
144143oveq2d 6294 . . . 4 g g g
145111, 144eqtrd 2443 . . 3 g g
146110, 145jca 530 . 2 g g
1478, 146rexlimddv 2900 1 g
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405   wcel 1842  wrex 2755  crab 2758  cvv 3059   cdif 3411   cun 3412   cin 3413   wss 3414  c0 3738  csn 3972   class class class wbr 4395   cmpt 4453  ccnv 4822   cdm 4823   crn 4824   cres 4825  cima 4826  wf 5565  cfv 5569  (class class class)co 6278  cixp 7507  cfn 7554  cbs 14841   cplusg 14909  c0g 15054   g cgsu 15055  cmnd 16243  cgrp 16377  SubGrpcsubg 16519  Cntzccntz 16677  clsm 16978  cpj1 16979   DProd cdprd 17344  dProjcdpj 17345 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-inf2 8091  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6521  df-om 6684  df-1st 6784  df-2nd 6785  df-supp 6903  df-tpos 6958  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-map 7459  df-ixp 7508  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fsupp 7864  df-oi 7969  df-card 8352  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-nn 10577  df-2 10635  df-n0 10837  df-z 10906  df-uz 11128  df-fz 11727  df-fzo 11855  df-seq 12152  df-hash 12453  df-ndx 14844  df-slot 14845  df-base 14846  df-sets 14847  df-ress 14848  df-plusg 14922  df-0g 15056  df-gsum 15057  df-mre 15200  df-mrc 15201  df-acs 15203  df-mgm 16196  df-sgrp 16235  df-mnd 16245  df-mhm 16290  df-submnd 16291  df-grp 16381  df-minusg 16382  df-sbg 16383  df-mulg 16384  df-subg 16522  df-ghm 16589  df-gim 16631  df-cntz 16679  df-oppg 16705  df-lsm 16980  df-pj1 16981  df-cmn 17124  df-dprd 17346  df-dpj 17347 This theorem is referenced by:  dpjeqOLD  17435
 Copyright terms: Public domain W3C validator