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 eqtrdi φ 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 19 difexd φ I x V
78 77 mptexd φ k I x f k V
79 78 ad2antrr φ f W A = G f x I k I x f k V
80 funmpt Fun k I x f k
81 80 a1i φ f W A = G f x I Fun k I x f k
82 25 adantr φ f W A = G f x I finSupp 0 ˙ f
83 ssdif I x I I x supp 0 ˙ f I supp 0 ˙ f
84 57 83 ax-mp I x supp 0 ˙ f I supp 0 ˙ f
85 84 sseli k I x supp 0 ˙ f k I supp 0 ˙ f
86 ssidd φ f W A = G f x I f supp 0 ˙ f supp 0 ˙
87 19 ad2antrr φ f W A = G f x I I V
88 5 fvexi 0 ˙ V
89 88 a1i φ f W A = G f x I 0 ˙ V
90 65 86 87 89 suppssr φ f W A = G f x I k I supp 0 ˙ f f k = 0 ˙
91 85 90 sylan2 φ f W A = G f x I k I x supp 0 ˙ f f k = 0 ˙
92 77 ad2antrr φ f W A = G f x I I x V
93 91 92 suppss2 φ f W A = G f x I k I x f k supp 0 ˙ f supp 0 ˙
94 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
95 79 81 82 93 94 syl22anc φ f W A = G f x I finSupp 0 ˙ k I x f k
96 56 60 64 76 95 dprdwd φ f W A = G f x I k I x f k h i I x S I x i | finSupp 0 ˙ h
97 70 96 eqeltrd φ f W A = G f x I f I x h i I x S I x i | finSupp 0 ˙ h
98 5 56 60 64 97 eldprdi φ f W A = G f x I G f I x G DProd S I x
99 26 98 sylan2 φ f W A = G f x I supp 0 ˙ f G f I x G DProd S I x
100 55 99 eqeltrd φ f W A = G f x I supp 0 ˙ f A G DProd S I x
101 eqid + G = + G
102 eqid LSSum G = LSSum G
103 61 15 ffvelrnd φ f W A = G f x I S x SubGrp G
104 dprdsubg G dom DProd S I x G DProd S I x SubGrp G
105 60 104 syl φ f W A = G f x I G DProd S I x SubGrp G
106 13 14 15 5 dpjdisj φ f W A = G f x I S x G DProd S I x = 0 ˙
107 13 14 15 33 dpjcntz φ f W A = G f x I S x Cntz G G DProd S I x
108 101 102 5 33 103 105 106 107 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 ˙
109 26 108 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 ˙
110 100 109 mpdan φ f W A = G f x I supp 0 ˙ f S x proj 1 G G DProd S I x A = 0 ˙
111 30 110 eqtrd φ f W A = G f x I supp 0 ˙ f P x A = 0 ˙
112 19 adantr φ f W A = G f I V
113 111 112 suppss2 φ f W A = G f x I P x A supp 0 ˙ f supp 0 ˙
114 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
115 21 23 25 113 114 syl22anc φ f W A = G f finSupp 0 ˙ x I P x A
116 6 11 12 18 115 dprdwd φ f W A = G f x I P x A W
117 simprr φ f W A = G f A = G f
118 39 feqmptd φ f W A = G f f = x I f x
119 simplrr φ f W A = G f x I A = G f
120 13 34 35 3syl φ f W A = G f x I G Mnd
121 6 13 14 41 dprdffsupp φ f W A = G f x I finSupp 0 ˙ f
122 disjdif x I x =
123 122 a1i φ f W A = G f x I x I x =
124 undif2 x I x = x I
125 15 snssd φ f W A = G f x I x I
126 ssequn1 x I x I = I
127 125 126 sylib φ f W A = G f x I x I = I
128 124 127 eqtr2id φ f W A = G f x I I = x I x
129 32 5 101 33 120 87 65 42 121 123 128 gsumzsplit φ f W A = G f x I G f = G f x + G G f I x
130 65 125 feqresmpt φ f W A = G f x I f x = k x f k
131 130 oveq2d φ f W A = G f x I G f x = G k x f k
132 65 15 ffvelrnd φ f W A = G f x I f x Base G
133 fveq2 k = x f k = f x
134 32 133 gsumsn G Mnd x I f x Base G G k x f k = f x
135 120 15 132 134 syl3anc φ f W A = G f x I G k x f k = f x
136 131 135 eqtrd φ f W A = G f x I G f x = f x
137 136 oveq1d φ f W A = G f x I G f x + G G f I x = f x + G G f I x
138 119 129 137 3eqtrd φ f W A = G f x I A = f x + G G f I x
139 13 14 15 102 dpjlsm φ f W A = G f x I G DProd S = S x LSSum G G DProd S I x
140 17 139 eleqtrd φ f W A = G f x I A S x LSSum G G DProd S I x
141 6 11 12 24 dprdfcl φ f W A = G f x I f x S x
142 101 102 5 33 103 105 106 107 27 140 141 98 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
143 138 142 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
144 143 simpld φ f W A = G f x I S x proj 1 G G DProd S I x A = f x
145 29 144 eqtrd φ f W A = G f x I P x A = f x
146 145 mpteq2dva φ f W A = G f x I P x A = x I f x
147 118 146 eqtr4d φ f W A = G f f = x I P x A
148 147 oveq2d φ f W A = G f G f = G x I P x A
149 117 148 eqtrd φ f W A = G f A = G x I P x A
150 116 149 jca φ f W A = G f x I P x A W A = G x I P x A
151 10 150 rexlimddv φ x I P x A W A = G x I P x A