Metamath Proof Explorer


Theorem dpjidcl

Description: The key property of projections: the sum of all the projections of A is A . (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses dpjfval.1 φGdomDProdS
dpjfval.2 φdomS=I
dpjfval.p P=GdProjS
dpjidcl.3 φAGDProdS
dpjidcl.0 0˙=0G
dpjidcl.w W=hiISi|finSupp0˙h
Assertion dpjidcl φxIPxAWA=GxIPxA

Proof

Step Hyp Ref Expression
1 dpjfval.1 φGdomDProdS
2 dpjfval.2 φdomS=I
3 dpjfval.p P=GdProjS
4 dpjidcl.3 φAGDProdS
5 dpjidcl.0 0˙=0G
6 dpjidcl.w W=hiISi|finSupp0˙h
7 5 6 eldprd domS=IAGDProdSGdomDProdSfWA=Gf
8 2 7 syl φAGDProdSGdomDProdSfWA=Gf
9 4 8 mpbid φGdomDProdSfWA=Gf
10 9 simprd φfWA=Gf
11 1 adantr φfWA=GfGdomDProdS
12 2 adantr φfWA=GfdomS=I
13 1 ad2antrr φfWA=GfxIGdomDProdS
14 2 ad2antrr φfWA=GfxIdomS=I
15 simpr φfWA=GfxIxI
16 13 14 3 15 dpjf φfWA=GfxIPx:GDProdSSx
17 4 ad2antrr φfWA=GfxIAGDProdS
18 16 17 ffvelcdmd φfWA=GfxIPxASx
19 1 2 dprddomcld φIV
20 19 mptexd φxIPxAV
21 20 adantr φfWA=GfxIPxAV
22 funmpt FunxIPxA
23 22 a1i φfWA=GfFunxIPxA
24 simprl φfWA=GffW
25 6 11 12 24 dprdffsupp φfWA=GffinSupp0˙f
26 eldifi xIsupp0˙fxI
27 eqid proj1G=proj1G
28 13 14 3 27 15 dpjval φfWA=GfxIPx=Sxproj1GGDProdSIx
29 28 fveq1d φfWA=GfxIPxA=Sxproj1GGDProdSIxA
30 26 29 sylan2 φfWA=GfxIsupp0˙fPxA=Sxproj1GGDProdSIxA
31 simplrr φfWA=GfxIsupp0˙fA=Gf
32 eqid BaseG=BaseG
33 eqid CntzG=CntzG
34 dprdgrp GdomDProdSGGrp
35 grpmnd GGrpGMnd
36 11 34 35 3syl φfWA=GfGMnd
37 36 adantr φfWA=GfxIsupp0˙fGMnd
38 19 ad2antrr φfWA=GfxIsupp0˙fIV
39 6 11 12 24 32 dprdff φfWA=Gff:IBaseG
40 39 adantr φfWA=GfxIsupp0˙ff:IBaseG
41 24 adantr φfWA=GfxIfW
42 6 13 14 41 33 dprdfcntz φfWA=GfxIranfCntzGranf
43 26 42 sylan2 φfWA=GfxIsupp0˙franfCntzGranf
44 snssi xIsupp0˙fxIsupp0˙f
45 44 adantl φfWA=GfxIsupp0˙fxIsupp0˙f
46 45 difss2d φfWA=GfxIsupp0˙fxI
47 suppssdm fsupp0˙domf
48 47 39 fssdm φfWA=Gffsupp0˙I
49 48 adantr φfWA=GfxIsupp0˙ffsupp0˙I
50 ssconb xIfsupp0˙IxIsupp0˙ffsupp0˙Ix
51 46 49 50 syl2anc φfWA=GfxIsupp0˙fxIsupp0˙ffsupp0˙Ix
52 45 51 mpbid φfWA=GfxIsupp0˙ffsupp0˙Ix
53 25 adantr φfWA=GfxIsupp0˙ffinSupp0˙f
54 32 5 33 37 38 40 43 52 53 gsumzres φfWA=GfxIsupp0˙fGfIx=Gf
55 31 54 eqtr4d φfWA=GfxIsupp0˙fA=GfIx
56 eqid hiIxSIxi|finSupp0˙h=hiIxSIxi|finSupp0˙h
57 difss IxI
58 57 a1i φfWA=GfxIIxI
59 13 14 58 dprdres φfWA=GfxIGdomDProdSIxGDProdSIxGDProdS
60 59 simpld φfWA=GfxIGdomDProdSIx
61 13 14 dprdf2 φfWA=GfxIS:ISubGrpG
62 fssres S:ISubGrpGIxISIx:IxSubGrpG
63 61 57 62 sylancl φfWA=GfxISIx:IxSubGrpG
64 63 fdmd φfWA=GfxIdomSIx=Ix
65 39 adantr φfWA=GfxIf:IBaseG
66 65 feqmptd φfWA=GfxIf=kIfk
67 66 reseq1d φfWA=GfxIfIx=kIfkIx
68 resmpt IxIkIfkIx=kIxfk
69 57 68 ax-mp kIfkIx=kIxfk
70 67 69 eqtrdi φfWA=GfxIfIx=kIxfk
71 eldifi kIxkI
72 6 13 14 41 dprdfcl φfWA=GfxIkIfkSk
73 71 72 sylan2 φfWA=GfxIkIxfkSk
74 fvres kIxSIxk=Sk
75 74 adantl φfWA=GfxIkIxSIxk=Sk
76 73 75 eleqtrrd φfWA=GfxIkIxfkSIxk
77 19 difexd φIxV
78 77 mptexd φkIxfkV
79 78 ad2antrr φfWA=GfxIkIxfkV
80 funmpt FunkIxfk
81 80 a1i φfWA=GfxIFunkIxfk
82 25 adantr φfWA=GfxIfinSupp0˙f
83 ssdif IxIIxsupp0˙fIsupp0˙f
84 57 83 ax-mp Ixsupp0˙fIsupp0˙f
85 84 sseli kIxsupp0˙fkIsupp0˙f
86 ssidd φfWA=GfxIfsupp0˙fsupp0˙
87 19 ad2antrr φfWA=GfxIIV
88 5 fvexi 0˙V
89 88 a1i φfWA=GfxI0˙V
90 65 86 87 89 suppssr φfWA=GfxIkIsupp0˙ffk=0˙
91 85 90 sylan2 φfWA=GfxIkIxsupp0˙ffk=0˙
92 77 ad2antrr φfWA=GfxIIxV
93 91 92 suppss2 φfWA=GfxIkIxfksupp0˙fsupp0˙
94 fsuppsssupp kIxfkVFunkIxfkfinSupp0˙fkIxfksupp0˙fsupp0˙finSupp0˙kIxfk
95 79 81 82 93 94 syl22anc φfWA=GfxIfinSupp0˙kIxfk
96 56 60 64 76 95 dprdwd φfWA=GfxIkIxfkhiIxSIxi|finSupp0˙h
97 70 96 eqeltrd φfWA=GfxIfIxhiIxSIxi|finSupp0˙h
98 5 56 60 64 97 eldprdi φfWA=GfxIGfIxGDProdSIx
99 26 98 sylan2 φfWA=GfxIsupp0˙fGfIxGDProdSIx
100 55 99 eqeltrd φfWA=GfxIsupp0˙fAGDProdSIx
101 eqid +G=+G
102 eqid LSSumG=LSSumG
103 61 15 ffvelcdmd φfWA=GfxISxSubGrpG
104 dprdsubg GdomDProdSIxGDProdSIxSubGrpG
105 60 104 syl φfWA=GfxIGDProdSIxSubGrpG
106 13 14 15 5 dpjdisj φfWA=GfxISxGDProdSIx=0˙
107 13 14 15 33 dpjcntz φfWA=GfxISxCntzGGDProdSIx
108 101 102 5 33 103 105 106 107 27 pj1rid φfWA=GfxIAGDProdSIxSxproj1GGDProdSIxA=0˙
109 26 108 sylanl2 φfWA=GfxIsupp0˙fAGDProdSIxSxproj1GGDProdSIxA=0˙
110 100 109 mpdan φfWA=GfxIsupp0˙fSxproj1GGDProdSIxA=0˙
111 30 110 eqtrd φfWA=GfxIsupp0˙fPxA=0˙
112 19 adantr φfWA=GfIV
113 111 112 suppss2 φfWA=GfxIPxAsupp0˙fsupp0˙
114 fsuppsssupp xIPxAVFunxIPxAfinSupp0˙fxIPxAsupp0˙fsupp0˙finSupp0˙xIPxA
115 21 23 25 113 114 syl22anc φfWA=GffinSupp0˙xIPxA
116 6 11 12 18 115 dprdwd φfWA=GfxIPxAW
117 simprr φfWA=GfA=Gf
118 39 feqmptd φfWA=Gff=xIfx
119 simplrr φfWA=GfxIA=Gf
120 13 34 35 3syl φfWA=GfxIGMnd
121 6 13 14 41 dprdffsupp φfWA=GfxIfinSupp0˙f
122 disjdif xIx=
123 122 a1i φfWA=GfxIxIx=
124 undif2 xIx=xI
125 15 snssd φfWA=GfxIxI
126 ssequn1 xIxI=I
127 125 126 sylib φfWA=GfxIxI=I
128 124 127 eqtr2id φfWA=GfxII=xIx
129 32 5 101 33 120 87 65 42 121 123 128 gsumzsplit φfWA=GfxIGf=Gfx+GGfIx
130 65 125 feqresmpt φfWA=GfxIfx=kxfk
131 130 oveq2d φfWA=GfxIGfx=Gkxfk
132 65 15 ffvelcdmd φfWA=GfxIfxBaseG
133 fveq2 k=xfk=fx
134 32 133 gsumsn GMndxIfxBaseGGkxfk=fx
135 120 15 132 134 syl3anc φfWA=GfxIGkxfk=fx
136 131 135 eqtrd φfWA=GfxIGfx=fx
137 136 oveq1d φfWA=GfxIGfx+GGfIx=fx+GGfIx
138 119 129 137 3eqtrd φfWA=GfxIA=fx+GGfIx
139 13 14 15 102 dpjlsm φfWA=GfxIGDProdS=SxLSSumGGDProdSIx
140 17 139 eleqtrd φfWA=GfxIASxLSSumGGDProdSIx
141 6 11 12 24 dprdfcl φfWA=GfxIfxSx
142 101 102 5 33 103 105 106 107 27 140 141 98 pj1eq φfWA=GfxIA=fx+GGfIxSxproj1GGDProdSIxA=fxGDProdSIxproj1GSxA=GfIx
143 138 142 mpbid φfWA=GfxISxproj1GGDProdSIxA=fxGDProdSIxproj1GSxA=GfIx
144 143 simpld φfWA=GfxISxproj1GGDProdSIxA=fx
145 29 144 eqtrd φfWA=GfxIPxA=fx
146 145 mpteq2dva φfWA=GfxIPxA=xIfx
147 118 146 eqtr4d φfWA=Gff=xIPxA
148 147 oveq2d φfWA=GfGf=GxIPxA
149 117 148 eqtrd φfWA=GfA=GxIPxA
150 116 149 jca φfWA=GfxIPxAWA=GxIPxA
151 10 150 rexlimddv φxIPxAWA=GxIPxA