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 φ G dom DProd S
dpjfval.2 φ dom S = I
dpjfval.p P = G dProj S
dpjidcl.3 φ A G DProd S
dpjidcl.0 0 ˙ = 0 G
dpjidcl.w W = h i I S i | finSupp 0 ˙ h
Assertion dpjidcl φ x I P x A W A = G x I P x A

Proof

Step Hyp Ref Expression
1 dpjfval.1 φ G dom DProd S
2 dpjfval.2 φ dom S = I
3 dpjfval.p P = G dProj S
4 dpjidcl.3 φ A G DProd S
5 dpjidcl.0 0 ˙ = 0 G
6 dpjidcl.w W = h i I S i | finSupp 0 ˙ h
7 5 6 eldprd dom S = I A G DProd S G dom DProd S f W A = G f
8 2 7 syl φ A G DProd S G dom DProd S f W A = G f
9 4 8 mpbid φ G dom DProd S f W A = G f
10 9 simprd φ f W A = G f
11 1 adantr φ f W A = G f G dom DProd S
12 2 adantr φ f W A = G f dom S = I
13 1 ad2antrr φ f W A = G f x I G dom DProd S
14 2 ad2antrr φ f W A = G f x I dom S = I
15 simpr φ f W A = G f x I x I
16 13 14 3 15 dpjf φ f W A = G f x I P x : G DProd S S x
17 4 ad2antrr φ f W A = G f x I A G DProd S
18 16 17 ffvelrnd φ f W A = G f x I P x A S x
19 1 2 dprddomcld φ I V
20 19 mptexd φ x I P x A V
21 20 adantr φ f W A = G f x I P x A V
22 funmpt Fun x I P x A
23 22 a1i φ f W A = G f Fun x I P x A
24 simprl φ f W A = G f f W
25 6 11 12 24 dprdffsupp φ f W A = G f finSupp 0 ˙ f
26 eldifi x I supp 0 ˙ f x I
27 eqid proj 1 G = proj 1 G
28 13 14 3 27 15 dpjval φ f W A = G f x I P x = S x proj 1 G G DProd S I x
29 28 fveq1d φ f W A = G f x I P x A = S x proj 1 G G DProd S I x A
30 26 29 sylan2 φ f W A = G f x I supp 0 ˙ f P x A = S x proj 1 G G DProd S I x A
31 simplrr φ f W A = G f x I supp 0 ˙ f A = G f
32 eqid Base G = Base G
33 eqid Cntz G = Cntz G
34 dprdgrp G dom DProd S G Grp
35 grpmnd G Grp G Mnd
36 11 34 35 3syl φ f W A = G f G Mnd
37 36 adantr φ f W A = G f x I supp 0 ˙ f G Mnd
38 19 ad2antrr φ f W A = G f x I supp 0 ˙ f I V
39 6 11 12 24 32 dprdff φ f W A = G f f : I Base G
40 39 adantr φ f W A = G f x I supp 0 ˙ f f : I Base G
41 24 adantr φ f W A = G f x I f W
42 6 13 14 41 33 dprdfcntz φ f W A = G f x I ran f Cntz G ran f
43 26 42 sylan2 φ f W A = G f x I supp 0 ˙ f ran f Cntz G ran f
44 snssi x I supp 0 ˙ f x I supp 0 ˙ f
45 44 adantl φ f W A = G f x I supp 0 ˙ f x I supp 0 ˙ f
46 45 difss2d φ f W A = G f x I supp 0 ˙ f x I
47 suppssdm f supp 0 ˙ dom f
48 47 39 fssdm φ f W A = G f f supp 0 ˙ I
49 48 adantr φ f W A = G f x I supp 0 ˙ f f supp 0 ˙ I
50 ssconb x I f supp 0 ˙ I x I supp 0 ˙ f f supp 0 ˙ I x
51 46 49 50 syl2anc φ f W A = G f x I supp 0 ˙ f x I supp 0 ˙ f f supp 0 ˙ I x
52 45 51 mpbid φ f W A = G f x I supp 0 ˙ f f supp 0 ˙ I x
53 25 adantr φ f W A = G f x I supp 0 ˙ f finSupp 0 ˙ f
54 32 5 33 37 38 40 43 52 53 gsumzres φ f W A = G f x I supp 0 ˙ f G f I x = G f
55 31 54 eqtr4d φ f W A = G f x I supp 0 ˙ f A = G f I x
56 eqid h i I x S I x i | finSupp 0 ˙ h = h i I x S I x i | finSupp 0 ˙ h
57 difss I x I
58 57 a1i φ f W A = G f x I I x I
59 13 14 58 dprdres φ f W A = G f x I G dom DProd S I x G DProd S I x G DProd S
60 59 simpld φ f W A = G f x I G dom DProd S I x
61 13 14 dprdf2 φ f W A = G f x I S : I SubGrp G
62 fssres S : I SubGrp G I x I S I x : I x SubGrp G
63 61 57 62 sylancl φ f W A = G f x I S I x : I x SubGrp G
64 63 fdmd φ f W A = G f x I dom S I x = I x
65 39 adantr φ f W A = G f x I f : I Base G
66 65 feqmptd φ f W A = G f x I f = k I f k
67 66 reseq1d φ f W A = G f x I f I x = k I f k I x
68 resmpt I x I k I f k I x = k I x f k
69 57 68 ax-mp k I f k I x = k I x f k
70 67 69 syl6eq φ f W A = G f x I f I x = k I x f k
71 eldifi k I x k I
72 6 13 14 41 dprdfcl φ f W A = G f x I k I f k S k
73 71 72 sylan2 φ f W A = G f x I k I x f k S k
74 fvres k I x S I x k = S k
75 74 adantl φ f W A = G f x I k I x S I x k = S k
76 73 75 eleqtrrd φ f W A = G f x I k I x f k S I x k
77 difexg I V I x V
78 19 77 syl φ I x V
79 78 mptexd φ k I x f k V
80 79 ad2antrr φ f W A = G f x I k I x f k V
81 funmpt Fun k I x f k
82 81 a1i φ f W A = G f x I Fun k I x f k
83 25 adantr φ f W A = G f x I finSupp 0 ˙ f
84 ssdif I x I I x supp 0 ˙ f I supp 0 ˙ f
85 57 84 ax-mp I x supp 0 ˙ f I supp 0 ˙ f
86 85 sseli k I x supp 0 ˙ f k I supp 0 ˙ f
87 ssidd φ f W A = G f x I f supp 0 ˙ f supp 0 ˙
88 19 ad2antrr φ f W A = G f x I I V
89 5 fvexi 0 ˙ V
90 89 a1i φ f W A = G f x I 0 ˙ V
91 65 87 88 90 suppssr φ f W A = G f x I k I supp 0 ˙ f f k = 0 ˙
92 86 91 sylan2 φ f W A = G f x I k I x supp 0 ˙ f f k = 0 ˙
93 78 ad2antrr φ f W A = G f x I I x V
94 92 93 suppss2 φ f W A = G f x I k I x f k supp 0 ˙ f supp 0 ˙
95 fsuppsssupp k I x f k V Fun k I x f k finSupp 0 ˙ f k I x f k supp 0 ˙ f supp 0 ˙ finSupp 0 ˙ k I x f k
96 80 82 83 94 95 syl22anc φ f W A = G f x I finSupp 0 ˙ k I x f k
97 56 60 64 76 96 dprdwd φ f W A = G f x I k I x f k h i I x S I x i | finSupp 0 ˙ h
98 70 97 eqeltrd φ f W A = G f x I f I x h i I x S I x i | finSupp 0 ˙ h
99 5 56 60 64 98 eldprdi φ f W A = G f x I G f I x G DProd S I x
100 26 99 sylan2 φ f W A = G f x I supp 0 ˙ f G f I x G DProd S I x
101 55 100 eqeltrd φ f W A = G f x I supp 0 ˙ f A G DProd S I x
102 eqid + G = + G
103 eqid LSSum G = LSSum G
104 61 15 ffvelrnd φ f W A = G f x I S x SubGrp G
105 dprdsubg G dom DProd S I x G DProd S I x SubGrp G
106 60 105 syl φ f W A = G f x I G DProd S I x SubGrp G
107 13 14 15 5 dpjdisj φ f W A = G f x I S x G DProd S I x = 0 ˙
108 13 14 15 33 dpjcntz φ f W A = G f x I S x Cntz G G DProd S I x
109 102 103 5 33 104 106 107 108 27 pj1rid φ f W A = G f x I A G DProd S I x S x proj 1 G G DProd S I x A = 0 ˙
110 26 109 sylanl2 φ f W A = G f x I supp 0 ˙ f A G DProd S I x S x proj 1 G G DProd S I x A = 0 ˙
111 101 110 mpdan φ f W A = G f x I supp 0 ˙ f S x proj 1 G G DProd S I x A = 0 ˙
112 30 111 eqtrd φ f W A = G f x I supp 0 ˙ f P x A = 0 ˙
113 19 adantr φ f W A = G f I V
114 112 113 suppss2 φ f W A = G f x I P x A supp 0 ˙ f supp 0 ˙
115 fsuppsssupp x I P x A V Fun x I P x A finSupp 0 ˙ f x I P x A supp 0 ˙ f supp 0 ˙ finSupp 0 ˙ x I P x A
116 21 23 25 114 115 syl22anc φ f W A = G f finSupp 0 ˙ x I P x A
117 6 11 12 18 116 dprdwd φ f W A = G f x I P x A W
118 simprr φ f W A = G f A = G f
119 39 feqmptd φ f W A = G f f = x I f x
120 simplrr φ f W A = G f x I A = G f
121 13 34 35 3syl φ f W A = G f x I G Mnd
122 6 13 14 41 dprdffsupp φ f W A = G f x I finSupp 0 ˙ f
123 disjdif x I x =
124 123 a1i φ f W A = G f x I x I x =
125 undif2 x I x = x I
126 15 snssd φ f W A = G f x I x I
127 ssequn1 x I x I = I
128 126 127 sylib φ f W A = G f x I x I = I
129 125 128 syl5req φ f W A = G f x I I = x I x
130 32 5 102 33 121 88 65 42 122 124 129 gsumzsplit φ f W A = G f x I G f = G f x + G G f I x
131 65 126 feqresmpt φ f W A = G f x I f x = k x f k
132 131 oveq2d φ f W A = G f x I G f x = G k x f k
133 65 15 ffvelrnd φ f W A = G f x I f x Base G
134 fveq2 k = x f k = f x
135 32 134 gsumsn G Mnd x I f x Base G G k x f k = f x
136 121 15 133 135 syl3anc φ f W A = G f x I G k x f k = f x
137 132 136 eqtrd φ f W A = G f x I G f x = f x
138 137 oveq1d φ f W A = G f x I G f x + G G f I x = f x + G G f I x
139 120 130 138 3eqtrd φ f W A = G f x I A = f x + G G f I x
140 13 14 15 103 dpjlsm φ f W A = G f x I G DProd S = S x LSSum G G DProd S I x
141 17 140 eleqtrd φ f W A = G f x I A S x LSSum G G DProd S I x
142 6 11 12 24 dprdfcl φ f W A = G f x I f x S x
143 102 103 5 33 104 106 107 108 27 141 142 99 pj1eq φ f W A = G f x I A = f x + G G f I x S x proj 1 G G DProd S I x A = f x G DProd S I x proj 1 G S x A = G f I x
144 139 143 mpbid φ f W A = G f x I S x proj 1 G G DProd S I x A = f x G DProd S I x proj 1 G S x A = G f I x
145 144 simpld φ f W A = G f x I S x proj 1 G G DProd S I x A = f x
146 29 145 eqtrd φ f W A = G f x I P x A = f x
147 146 mpteq2dva φ f W A = G f x I P x A = x I f x
148 119 147 eqtr4d φ f W A = G f f = x I P x A
149 148 oveq2d φ f W A = G f G f = G x I P x A
150 118 149 eqtrd φ f W A = G f A = G x I P x A
151 117 150 jca φ f W A = G f x I P x A W A = G x I P x A
152 10 151 rexlimddv φ x I P x A W A = G x I P x A