Metamath Proof Explorer


Theorem elrspunidl

Description: Elementhood to the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypotheses elrspunidl.n N = RSpan R
elrspunidl.b B = Base R
elrspunidl.1 0 ˙ = 0 R
elrspunidl.x · ˙ = R
elrspunidl.r φ R Ring
elrspunidl.i φ S LIdeal R
Assertion elrspunidl φ X N S a B S finSupp 0 ˙ a X = R a k S a k k

Proof

Step Hyp Ref Expression
1 elrspunidl.n N = RSpan R
2 elrspunidl.b B = Base R
3 elrspunidl.1 0 ˙ = 0 R
4 elrspunidl.x · ˙ = R
5 elrspunidl.r φ R Ring
6 elrspunidl.i φ S LIdeal R
7 6 sselda φ i S i LIdeal R
8 eqid LIdeal R = LIdeal R
9 2 8 lidlss i LIdeal R i B
10 7 9 syl φ i S i B
11 10 ralrimiva φ i S i B
12 unissb S B i S i B
13 11 12 sylibr φ S B
14 1 2 3 4 5 13 elrsp φ X N S b B S finSupp 0 ˙ b X = R j S b j · ˙ j
15 fvexd φ LIdeal R V
16 15 6 ssexd φ S V
17 16 uniexd φ S V
18 eluni2 j S i S j i
19 18 biimpi j S i S j i
20 19 adantl φ j S i S j i
21 20 ralrimiva φ j S i S j i
22 eleq2 i = f j j i j f j
23 22 ac6sg S V j S i S j i f f : S S j S j f j
24 17 21 23 sylc φ f f : S S j S j f j
25 24 ad3antrrr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f f : S S j S j f j
26 simp-5l φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j φ
27 26 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S φ
28 ringcmn R Ring R CMnd
29 27 5 28 3syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R CMnd
30 vex f V
31 cnvexg f V f -1 V
32 imaexg f -1 V f -1 i V
33 30 31 32 mp2b f -1 i V
34 33 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f -1 i V
35 5 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i R Ring
36 elmapi b B S b : S B
37 36 ad7antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i b : S B
38 cnvimass f -1 i dom f
39 fdm f : S S dom f = S
40 38 39 sseqtrid f : S S f -1 i S
41 40 ad3antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f -1 i S
42 41 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i l S
43 37 42 ffvelrnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i b l B
44 13 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i S B
45 44 42 sseldd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i l B
46 2 4 ringcl R Ring b l B l B b l · ˙ l B
47 35 43 45 46 syl3anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S l f -1 i b l · ˙ l B
48 fveq2 j = l b j = b l
49 id j = l j = l
50 48 49 oveq12d j = l b j · ˙ j = b l · ˙ l
51 50 cbvmptv j f -1 i b j · ˙ j = l f -1 i b l · ˙ l
52 47 51 fmptd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i b j · ˙ j : f -1 i B
53 34 mptexd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i b j · ˙ j V
54 52 ffund φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S Fun j f -1 i b j · ˙ j
55 simp-5r φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S finSupp 0 ˙ b
56 nfv j φ b B S finSupp 0 ˙ b
57 nfcv _ j R
58 nfcv _ j Σ𝑔
59 nfmpt1 _ j j S b j · ˙ j
60 57 58 59 nfov _ j R j S b j · ˙ j
61 60 nfeq2 j X = R j S b j · ˙ j
62 56 61 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j
63 nfv j f : S S
64 62 63 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S
65 nfra1 j j S j f j
66 64 65 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j
67 nfv j i S
68 66 67 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S
69 nfcv _ j f -1 i
70 nfcv _ j supp 0 ˙ b
71 36 ad7antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b b : S B
72 71 ffnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b b Fn S
73 26 17 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j S V
74 73 ad2antrr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b S V
75 3 fvexi 0 ˙ V
76 75 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b 0 ˙ V
77 41 ssdifd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f -1 i supp 0 ˙ b S supp 0 ˙ b
78 77 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b j S supp 0 ˙ b
79 72 74 76 78 fvdifsupp φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b b j = 0 ˙
80 79 oveq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b b j · ˙ j = 0 ˙ · ˙ j
81 5 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b R Ring
82 13 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b S B
83 78 eldifad φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b j S
84 82 83 sseldd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b j B
85 2 4 3 ringlz R Ring j B 0 ˙ · ˙ j = 0 ˙
86 81 84 85 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b 0 ˙ · ˙ j = 0 ˙
87 80 86 eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i supp 0 ˙ b b j · ˙ j = 0 ˙
88 68 69 70 87 34 suppss2f φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j f -1 i b j · ˙ j supp 0 ˙ b supp 0 ˙
89 fsuppsssupp j f -1 i b j · ˙ j V Fun j f -1 i b j · ˙ j finSupp 0 ˙ b j f -1 i b j · ˙ j supp 0 ˙ b supp 0 ˙ finSupp 0 ˙ j f -1 i b j · ˙ j
90 53 54 55 88 89 syl22anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S finSupp 0 ˙ j f -1 i b j · ˙ j
91 2 3 29 34 52 90 gsumcl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j B
92 91 fmpttd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j : S B
93 2 fvexi B V
94 93 a1i φ B V
95 94 16 elmapd φ i S R j f -1 i b j · ˙ j B S i S R j f -1 i b j · ˙ j : S B
96 95 biimpar φ i S R j f -1 i b j · ˙ j : S B i S R j f -1 i b j · ˙ j B S
97 26 92 96 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j B S
98 breq1 a = i S R j f -1 i b j · ˙ j finSupp 0 ˙ a finSupp 0 ˙ i S R j f -1 i b j · ˙ j
99 oveq2 a = i S R j f -1 i b j · ˙ j R a = R i S R j f -1 i b j · ˙ j
100 99 eqeq2d a = i S R j f -1 i b j · ˙ j X = R a X = R i S R j f -1 i b j · ˙ j
101 fveq1 a = i S R j f -1 i b j · ˙ j a k = i S R j f -1 i b j · ˙ j k
102 101 eleq1d a = i S R j f -1 i b j · ˙ j a k k i S R j f -1 i b j · ˙ j k k
103 102 ralbidv a = i S R j f -1 i b j · ˙ j k S a k k k S i S R j f -1 i b j · ˙ j k k
104 98 100 103 3anbi123d a = i S R j f -1 i b j · ˙ j finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ i S R j f -1 i b j · ˙ j X = R i S R j f -1 i b j · ˙ j k S i S R j f -1 i b j · ˙ j k k
105 104 adantl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j a = i S R j f -1 i b j · ˙ j finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ i S R j f -1 i b j · ˙ j X = R i S R j f -1 i b j · ˙ j k S i S R j f -1 i b j · ˙ j k k
106 26 16 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j S V
107 106 mptexd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j V
108 75 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j 0 ˙ V
109 funmpt Fun i S R j f -1 i b j · ˙ j
110 109 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j Fun i S R j f -1 i b j · ˙ j
111 simplr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j f : S S
112 111 ffund φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j Fun f
113 simp-4r φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j finSupp 0 ˙ b
114 113 fsuppimpd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j b supp 0 ˙ Fin
115 imafi Fun f b supp 0 ˙ Fin f b supp 0 ˙ Fin
116 112 114 115 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j f b supp 0 ˙ Fin
117 nfv j i S f b supp 0 ˙
118 66 117 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙
119 simpllr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f : S S
120 119 ffund φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ Fun f
121 snssi i S f b supp 0 ˙ i S f b supp 0 ˙
122 121 adantl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ i S f b supp 0 ˙
123 sspreima Fun f i S f b supp 0 ˙ f -1 i f -1 S f b supp 0 ˙
124 120 122 123 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 i f -1 S f b supp 0 ˙
125 difpreima Fun f f -1 S f b supp 0 ˙ = f -1 S f -1 f b supp 0 ˙
126 120 125 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 S f b supp 0 ˙ = f -1 S f -1 f b supp 0 ˙
127 124 126 sseqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 i f -1 S f -1 f b supp 0 ˙
128 suppssdm b supp 0 ˙ dom b
129 36 ad6antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ b : S B
130 128 129 fssdm φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ b supp 0 ˙ S
131 119 fdmd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ dom f = S
132 130 131 sseqtrrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ b supp 0 ˙ dom f
133 sseqin2 b supp 0 ˙ dom f dom f supp 0 ˙ b = b supp 0 ˙
134 133 biimpi b supp 0 ˙ dom f dom f supp 0 ˙ b = b supp 0 ˙
135 dminss dom f supp 0 ˙ b f -1 f b supp 0 ˙
136 134 135 eqsstrrdi b supp 0 ˙ dom f b supp 0 ˙ f -1 f b supp 0 ˙
137 132 136 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ b supp 0 ˙ f -1 f b supp 0 ˙
138 137 sscond φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 S f -1 f b supp 0 ˙ f -1 S supp 0 ˙ b
139 127 138 sstrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 i f -1 S supp 0 ˙ b
140 fimacnv f : S S f -1 S = S
141 119 140 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 S = S
142 141 difeq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 S supp 0 ˙ b = S supp 0 ˙ b
143 139 142 sseqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 i S supp 0 ˙ b
144 143 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i j S supp 0 ˙ b
145 ssidd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ b supp 0 ˙ b supp 0 ˙
146 73 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ S V
147 75 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ 0 ˙ V
148 129 145 146 147 suppssr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j S supp 0 ˙ b b j = 0 ˙
149 144 148 syldan φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i b j = 0 ˙
150 149 oveq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i b j · ˙ j = 0 ˙ · ˙ j
151 5 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i R Ring
152 13 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i S B
153 40 ad3antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ f -1 i S
154 153 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i j S
155 152 154 sseldd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i j B
156 151 155 85 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i 0 ˙ · ˙ j = 0 ˙
157 150 156 eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i b j · ˙ j = 0 ˙
158 118 157 mpteq2da φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ j f -1 i b j · ˙ j = j f -1 i 0 ˙
159 158 oveq2d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ R j f -1 i b j · ˙ j = R j f -1 i 0 ˙
160 5 28 syl φ R CMnd
161 160 cmnmndd φ R Mnd
162 161 ad6antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ R Mnd
163 3 gsumz R Mnd f -1 i V R j f -1 i 0 ˙ = 0 ˙
164 162 33 163 sylancl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ R j f -1 i 0 ˙ = 0 ˙
165 159 164 eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f b supp 0 ˙ R j f -1 i b j · ˙ j = 0 ˙
166 165 106 suppss2 φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j supp 0 ˙ f b supp 0 ˙
167 116 166 ssfid φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j f -1 i b j · ˙ j supp 0 ˙ Fin
168 isfsupp i S R j f -1 i b j · ˙ j V 0 ˙ V finSupp 0 ˙ i S R j f -1 i b j · ˙ j Fun i S R j f -1 i b j · ˙ j i S R j f -1 i b j · ˙ j supp 0 ˙ Fin
169 168 biimpar i S R j f -1 i b j · ˙ j V 0 ˙ V Fun i S R j f -1 i b j · ˙ j i S R j f -1 i b j · ˙ j supp 0 ˙ Fin finSupp 0 ˙ i S R j f -1 i b j · ˙ j
170 107 108 110 167 169 syl22anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j finSupp 0 ˙ i S R j f -1 i b j · ˙ j
171 simpllr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j X = R j S b j · ˙ j
172 26 160 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j R CMnd
173 5 ad6antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S R Ring
174 36 ad5antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j b : S B
175 174 ffvelrnda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S b j B
176 26 13 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j S B
177 176 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S j B
178 2 4 ringcl R Ring b j B j B b j · ˙ j B
179 173 175 177 178 syl3anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S b j · ˙ j B
180 eqid j S b j · ˙ j = j S b j · ˙ j
181 66 179 180 fmptdf φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S b j · ˙ j : S B
182 73 mptexd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S b j · ˙ j V
183 funmpt Fun j S b j · ˙ j
184 183 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j Fun j S b j · ˙ j
185 nfcv _ j S
186 174 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b b : S B
187 186 ffnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b b Fn S
188 73 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b S V
189 75 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b 0 ˙ V
190 simpr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b j S supp 0 ˙ b
191 187 188 189 190 fvdifsupp φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b b j = 0 ˙
192 191 oveq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b b j · ˙ j = 0 ˙ · ˙ j
193 5 ad6antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b R Ring
194 176 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b S B
195 190 eldifad φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b j S
196 194 195 sseldd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b j B
197 193 196 85 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b 0 ˙ · ˙ j = 0 ˙
198 192 197 eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S supp 0 ˙ b b j · ˙ j = 0 ˙
199 66 185 70 198 73 suppss2f φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j j S b j · ˙ j supp 0 ˙ b supp 0 ˙
200 fsuppsssupp j S b j · ˙ j V Fun j S b j · ˙ j finSupp 0 ˙ b j S b j · ˙ j supp 0 ˙ b supp 0 ˙ finSupp 0 ˙ j S b j · ˙ j
201 182 184 113 199 200 syl22anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j finSupp 0 ˙ j S b j · ˙ j
202 sndisj Disj i S i
203 disjpreima Fun f Disj i S i Disj i S f -1 i
204 112 202 203 sylancl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j Disj i S f -1 i
205 iunid i S i = S
206 205 imaeq2i f -1 i S i = f -1 S
207 iunpreima Fun f f -1 i S i = i S f -1 i
208 112 207 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j f -1 i S i = i S f -1 i
209 140 ad2antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j f -1 S = S
210 206 208 209 3eqtr3a φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S f -1 i = S
211 2 3 172 73 106 181 201 204 210 gsumpart φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j R j S b j · ˙ j = R i S R j S b j · ˙ j f -1 i
212 41 resmptd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S j S b j · ˙ j f -1 i = j f -1 i b j · ˙ j
213 212 oveq2d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j S b j · ˙ j f -1 i = R j f -1 i b j · ˙ j
214 213 mpteq2dva φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j i S R j S b j · ˙ j f -1 i = i S R j f -1 i b j · ˙ j
215 214 oveq2d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j R i S R j S b j · ˙ j f -1 i = R i S R j f -1 i b j · ˙ j
216 171 211 215 3eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j X = R i S R j f -1 i b j · ˙ j
217 eqid i S R j f -1 i b j · ˙ j = i S R j f -1 i b j · ˙ j
218 simpr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i = k i = k
219 218 sneqd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i = k i = k
220 219 imaeq2d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i = k f -1 i = f -1 k
221 220 mpteq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i = k j f -1 i b j · ˙ j = j f -1 k b j · ˙ j
222 221 oveq2d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i = k R j f -1 i b j · ˙ j = R j f -1 k b j · ˙ j
223 simpr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S k S
224 ovexd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S R j f -1 k b j · ˙ j V
225 217 222 223 224 fvmptd2 φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i S R j f -1 i b j · ˙ j k = R j f -1 k b j · ˙ j
226 160 ad6antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S R CMnd
227 30 cnvex f -1 V
228 227 imaex f -1 k V
229 228 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S f -1 k V
230 5 ad6antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S R Ring
231 26 6 syl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j S LIdeal R
232 231 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S k LIdeal R
233 8 lidlsubg R Ring k LIdeal R k SubGrp R
234 subgsubm k SubGrp R k SubMnd R
235 233 234 syl R Ring k LIdeal R k SubMnd R
236 230 232 235 syl2anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S k SubMnd R
237 230 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k R Ring
238 232 adantr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k k LIdeal R
239 36 ad7antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k b : S B
240 cnvimass f -1 k dom f
241 240 39 sseqtrid f : S S f -1 k S
242 241 ad3antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S f -1 k S
243 242 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k l S
244 239 243 ffvelrnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k b l B
245 fveq2 j = l f j = f l
246 49 245 eleq12d j = l j f j l f l
247 simpllr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k j S j f j
248 246 247 243 rspcdva φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k l f l
249 simp-4r φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k f : S S
250 249 ffnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k f Fn S
251 elpreima f Fn S l f -1 k l S f l k
252 251 biimpa f Fn S l f -1 k l S f l k
253 elsni f l k f l = k
254 252 253 simpl2im f Fn S l f -1 k f l = k
255 250 254 sylancom φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k f l = k
256 248 255 eleqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k l k
257 8 2 4 lidlmcl R Ring k LIdeal R b l B l k b l · ˙ l k
258 237 238 244 256 257 syl22anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S l f -1 k b l · ˙ l k
259 50 cbvmptv j f -1 k b j · ˙ j = l f -1 k b l · ˙ l
260 258 259 fmptd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k b j · ˙ j : f -1 k k
261 229 mptexd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k b j · ˙ j V
262 260 ffund φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S Fun j f -1 k b j · ˙ j
263 simp-5r φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S finSupp 0 ˙ b
264 nfv j k S
265 66 264 nfan j φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S
266 nfcv _ j f -1 k
267 36 ad7antlr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b b : S B
268 267 ffnd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b b Fn S
269 73 ad2antrr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b S V
270 75 a1i φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b 0 ˙ V
271 242 ssdifd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S f -1 k supp 0 ˙ b S supp 0 ˙ b
272 271 sselda φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b j S supp 0 ˙ b
273 268 269 270 272 fvdifsupp φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b b j = 0 ˙
274 273 oveq1d φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b b j · ˙ j = 0 ˙ · ˙ j
275 13 ad7antr φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b S B
276 272 eldifad φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b j S
277 275 276 sseldd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b j B
278 230 277 85 syl2an2r φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b 0 ˙ · ˙ j = 0 ˙
279 274 278 eqtrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k supp 0 ˙ b b j · ˙ j = 0 ˙
280 265 266 70 279 229 suppss2f φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S j f -1 k b j · ˙ j supp 0 ˙ b supp 0 ˙
281 fsuppsssupp j f -1 k b j · ˙ j V Fun j f -1 k b j · ˙ j finSupp 0 ˙ b j f -1 k b j · ˙ j supp 0 ˙ b supp 0 ˙ finSupp 0 ˙ j f -1 k b j · ˙ j
282 261 262 263 280 281 syl22anc φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S finSupp 0 ˙ j f -1 k b j · ˙ j
283 3 226 229 236 260 282 gsumsubmcl φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S R j f -1 k b j · ˙ j k
284 225 283 eqeltrd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i S R j f -1 i b j · ˙ j k k
285 284 ralrimiva φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j k S i S R j f -1 i b j · ˙ j k k
286 170 216 285 3jca φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j finSupp 0 ˙ i S R j f -1 i b j · ˙ j X = R i S R j f -1 i b j · ˙ j k S i S R j f -1 i b j · ˙ j k k
287 97 105 286 rspcedvd φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j a B S finSupp 0 ˙ a X = R a k S a k k
288 287 anasss φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j f : S S j S j f j a B S finSupp 0 ˙ a X = R a k S a k k
289 25 288 exlimddv φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j a B S finSupp 0 ˙ a X = R a k S a k k
290 289 anasss φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j a B S finSupp 0 ˙ a X = R a k S a k k
291 290 r19.29an φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j a B S finSupp 0 ˙ a X = R a k S a k k
292 5 ad4antr φ a B S finSupp 0 ˙ a X = R a k S a k k R Ring
293 292 adantr φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ R Ring
294 eqid ℤRHom R = ℤRHom R
295 294 zrhrhm R Ring ℤRHom R ring RingHom R
296 zringbas = Base ring
297 296 2 rhmf ℤRHom R ring RingHom R ℤRHom R : B
298 293 295 297 3syl φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R : B
299 simp-5r φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ a B S
300 75 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ 0 ˙ V
301 ssv ran a V
302 ssdif ran a V ran a 0 ˙ V 0 ˙
303 301 302 ax-mp ran a 0 ˙ V 0 ˙
304 303 sseli m ran a 0 ˙ m V 0 ˙
305 304 adantl φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ m V 0 ˙
306 simp-4r φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ finSupp 0 ˙ a
307 299 300 305 306 fsuppinisegfi φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ a -1 m Fin
308 hashcl a -1 m Fin a -1 m 0
309 307 308 syl φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ a -1 m 0
310 309 nn0zd φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ a -1 m
311 298 310 ffvelrnd φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m B
312 eqid m ran a 0 ˙ ℤRHom R a -1 m = m ran a 0 ˙ ℤRHom R a -1 m
313 311 312 fmptd φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m : ran a 0 ˙ B
314 2 3 ring0cl R Ring 0 ˙ B
315 fconst6g 0 ˙ B S ran a 0 ˙ × 0 ˙ : S ran a 0 ˙ B
316 292 314 315 3syl φ a B S finSupp 0 ˙ a X = R a k S a k k S ran a 0 ˙ × 0 ˙ : S ran a 0 ˙ B
317 disjdif ran a 0 ˙ S ran a 0 ˙ =
318 317 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k ran a 0 ˙ S ran a 0 ˙ =
319 313 316 318 fun2d φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ : ran a 0 ˙ S ran a 0 ˙ B
320 simplll φ a B S finSupp 0 ˙ a X = R a k S a k k φ a B S
321 94 16 elmapd φ a B S a : S B
322 321 biimpa φ a B S a : S B
323 320 322 syl φ a B S finSupp 0 ˙ a X = R a k S a k k a : S B
324 323 ffnd φ a B S finSupp 0 ˙ a X = R a k S a k k a Fn S
325 elssuni k S k S
326 325 adantl φ a B S finSupp 0 ˙ a X = R a k S k S
327 326 sseld φ a B S finSupp 0 ˙ a X = R a k S a k k a k S
328 327 ralimdva φ a B S finSupp 0 ˙ a X = R a k S a k k k S a k S
329 328 imp φ a B S finSupp 0 ˙ a X = R a k S a k k k S a k S
330 fnfvrnss a Fn S k S a k S ran a S
331 324 329 330 syl2anc φ a B S finSupp 0 ˙ a X = R a k S a k k ran a S
332 331 ssdifssd φ a B S finSupp 0 ˙ a X = R a k S a k k ran a 0 ˙ S
333 undif ran a 0 ˙ S ran a 0 ˙ S ran a 0 ˙ = S
334 332 333 sylib φ a B S finSupp 0 ˙ a X = R a k S a k k ran a 0 ˙ S ran a 0 ˙ = S
335 334 feq2d φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ : ran a 0 ˙ S ran a 0 ˙ B m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ : S B
336 319 335 mpbid φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ : S B
337 93 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k B V
338 17 ad4antr φ a B S finSupp 0 ˙ a X = R a k S a k k S V
339 337 338 elmapd φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ B S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ : S B
340 336 339 mpbird φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ B S
341 breq1 b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ finSupp 0 ˙ b finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙
342 fveq1 b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ b j = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j
343 342 oveq1d b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ b j · ˙ j = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
344 343 mpteq2dv b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j S b j · ˙ j = j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
345 344 oveq2d b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ R j S b j · ˙ j = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
346 345 eqeq2d b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ X = R j S b j · ˙ j X = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
347 341 346 anbi12d b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ finSupp 0 ˙ b X = R j S b j · ˙ j finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ X = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
348 347 adantl φ a B S finSupp 0 ˙ a X = R a k S a k k b = m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ finSupp 0 ˙ b X = R j S b j · ˙ j finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ X = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
349 319 ffund φ a B S finSupp 0 ˙ a X = R a k S a k k Fun m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙
350 340 elexd φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ V
351 75 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k 0 ˙ V
352 323 ffund φ a B S finSupp 0 ˙ a X = R a k S a k k Fun a
353 320 simprd φ a B S finSupp 0 ˙ a X = R a k S a k k a B S
354 simpllr φ a B S finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ a
355 fsupprnfi Fun a a B S 0 ˙ V finSupp 0 ˙ a ran a Fin
356 diffi ran a Fin ran a 0 ˙ Fin
357 355 356 syl Fun a a B S 0 ˙ V finSupp 0 ˙ a ran a 0 ˙ Fin
358 352 353 351 354 357 syl22anc φ a B S finSupp 0 ˙ a X = R a k S a k k ran a 0 ˙ Fin
359 313 358 351 fdmfifsupp φ a B S finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m
360 13 ssdifssd φ S ran a 0 ˙ B
361 360 ad4antr φ a B S finSupp 0 ˙ a X = R a k S a k k S ran a 0 ˙ B
362 337 361 ssexd φ a B S finSupp 0 ˙ a X = R a k S a k k S ran a 0 ˙ V
363 362 351 fczfsuppd φ a B S finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ S ran a 0 ˙ × 0 ˙
364 359 363 fsuppun φ a B S finSupp 0 ˙ a X = R a k S a k k m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ supp 0 ˙ Fin
365 funisfsupp Fun m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ V 0 ˙ V finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ supp 0 ˙ Fin
366 365 biimpar Fun m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ V 0 ˙ V m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ supp 0 ˙ Fin finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙
367 349 350 351 364 366 syl31anc φ a B S finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙
368 fvex ℤRHom R a -1 m V
369 368 312 fnmpti m ran a 0 ˙ ℤRHom R a -1 m Fn ran a 0 ˙
370 369 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m Fn ran a 0 ˙
371 fnconstg 0 ˙ V S ran a 0 ˙ × 0 ˙ Fn S ran a 0 ˙
372 75 371 ax-mp S ran a 0 ˙ × 0 ˙ Fn S ran a 0 ˙
373 372 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ S ran a 0 ˙ × 0 ˙ Fn S ran a 0 ˙
374 317 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ ran a 0 ˙ S ran a 0 ˙ =
375 simpr φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ j ran a 0 ˙
376 370 373 374 375 fvun1d φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = m ran a 0 ˙ ℤRHom R a -1 m j
377 sneq m = j m = j
378 377 imaeq2d m = j a -1 m = a -1 j
379 378 fveq2d m = j a -1 m = a -1 j
380 379 fveq2d m = j ℤRHom R a -1 m = ℤRHom R a -1 j
381 fvexd φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ ℤRHom R a -1 j V
382 312 380 375 381 fvmptd3 φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m j = ℤRHom R a -1 j
383 376 382 eqtrd φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = ℤRHom R a -1 j
384 383 oveq1d φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = ℤRHom R a -1 j · ˙ j
385 384 mpteq2dva φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = j ran a 0 ˙ ℤRHom R a -1 j · ˙ j
386 385 oveq2d φ a B S finSupp 0 ˙ a X = R a k S a k k R j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = R j ran a 0 ˙ ℤRHom R a -1 j · ˙ j
387 292 28 syl φ a B S finSupp 0 ˙ a X = R a k S a k k R CMnd
388 317 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ ran a 0 ˙ S ran a 0 ˙ =
389 fvun2 m ran a 0 ˙ ℤRHom R a -1 m Fn ran a 0 ˙ S ran a 0 ˙ × 0 ˙ Fn S ran a 0 ˙ ran a 0 ˙ S ran a 0 ˙ = j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = S ran a 0 ˙ × 0 ˙ j
390 369 372 389 mp3an12 ran a 0 ˙ S ran a 0 ˙ = j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = S ran a 0 ˙ × 0 ˙ j
391 388 390 sylancom φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = S ran a 0 ˙ × 0 ˙ j
392 75 fvconst2 j S ran a 0 ˙ S ran a 0 ˙ × 0 ˙ j = 0 ˙
393 392 adantl φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ S ran a 0 ˙ × 0 ˙ j = 0 ˙
394 391 393 eqtrd φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j = 0 ˙
395 394 oveq1d φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = 0 ˙ · ˙ j
396 361 sselda φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ j B
397 292 396 85 syl2an2r φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ 0 ˙ · ˙ j = 0 ˙
398 395 397 eqtrd φ a B S finSupp 0 ˙ a X = R a k S a k k j S ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = 0 ˙
399 292 adantr φ a B S finSupp 0 ˙ a X = R a k S a k k j S R Ring
400 336 ffvelrnda φ a B S finSupp 0 ˙ a X = R a k S a k k j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j B
401 13 ad4antr φ a B S finSupp 0 ˙ a X = R a k S a k k S B
402 401 sselda φ a B S finSupp 0 ˙ a X = R a k S a k k j S j B
403 2 4 ringcl R Ring m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j B j B m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j B
404 399 400 402 403 syl3anc φ a B S finSupp 0 ˙ a X = R a k S a k k j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j B
405 2 3 387 338 398 358 404 332 gsummptres2 φ a B S finSupp 0 ˙ a X = R a k S a k k R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j = R j ran a 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
406 eqid R = R
407 2 3 406 387 323 354 gsumhashmul φ a B S finSupp 0 ˙ a X = R a k S a k k R a = R j ran a 0 ˙ a -1 j R j
408 simplr φ a B S finSupp 0 ˙ a X = R a k S a k k X = R a
409 292 adantr φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ R Ring
410 353 adantr φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ a B S
411 75 a1i φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ 0 ˙ V
412 303 375 sselid φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ j V 0 ˙
413 354 adantr φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ finSupp 0 ˙ a
414 410 411 412 413 fsuppinisegfi φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ a -1 j Fin
415 hashcl a -1 j Fin a -1 j 0
416 414 415 syl φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ a -1 j 0
417 416 nn0zd φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ a -1 j
418 332 401 sstrd φ a B S finSupp 0 ˙ a X = R a k S a k k ran a 0 ˙ B
419 418 sselda φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ j B
420 eqid 1 R = 1 R
421 294 406 420 zrhmulg R Ring a -1 j ℤRHom R a -1 j = a -1 j R 1 R
422 421 adantr R Ring a -1 j j B ℤRHom R a -1 j = a -1 j R 1 R
423 422 oveq1d R Ring a -1 j j B ℤRHom R a -1 j · ˙ j = a -1 j R 1 R · ˙ j
424 simpll R Ring a -1 j j B R Ring
425 simplr R Ring a -1 j j B a -1 j
426 2 420 ringidcl R Ring 1 R B
427 426 ad2antrr R Ring a -1 j j B 1 R B
428 simpr R Ring a -1 j j B j B
429 2 406 4 mulgass2 R Ring a -1 j 1 R B j B a -1 j R 1 R · ˙ j = a -1 j R 1 R · ˙ j
430 424 425 427 428 429 syl13anc R Ring a -1 j j B a -1 j R 1 R · ˙ j = a -1 j R 1 R · ˙ j
431 2 4 420 ringlidm R Ring j B 1 R · ˙ j = j
432 424 431 sylancom R Ring a -1 j j B 1 R · ˙ j = j
433 432 oveq2d R Ring a -1 j j B a -1 j R 1 R · ˙ j = a -1 j R j
434 423 430 433 3eqtrd R Ring a -1 j j B ℤRHom R a -1 j · ˙ j = a -1 j R j
435 409 417 419 434 syl21anc φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ ℤRHom R a -1 j · ˙ j = a -1 j R j
436 435 mpteq2dva φ a B S finSupp 0 ˙ a X = R a k S a k k j ran a 0 ˙ ℤRHom R a -1 j · ˙ j = j ran a 0 ˙ a -1 j R j
437 436 oveq2d φ a B S finSupp 0 ˙ a X = R a k S a k k R j ran a 0 ˙ ℤRHom R a -1 j · ˙ j = R j ran a 0 ˙ a -1 j R j
438 407 408 437 3eqtr4d φ a B S finSupp 0 ˙ a X = R a k S a k k X = R j ran a 0 ˙ ℤRHom R a -1 j · ˙ j
439 386 405 438 3eqtr4rd φ a B S finSupp 0 ˙ a X = R a k S a k k X = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
440 367 439 jca φ a B S finSupp 0 ˙ a X = R a k S a k k finSupp 0 ˙ m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ X = R j S m ran a 0 ˙ ℤRHom R a -1 m S ran a 0 ˙ × 0 ˙ j · ˙ j
441 340 348 440 rspcedvd φ a B S finSupp 0 ˙ a X = R a k S a k k b B S finSupp 0 ˙ b X = R j S b j · ˙ j
442 441 exp41 φ a B S finSupp 0 ˙ a X = R a k S a k k b B S finSupp 0 ˙ b X = R j S b j · ˙ j
443 442 3imp2 φ a B S finSupp 0 ˙ a X = R a k S a k k b B S finSupp 0 ˙ b X = R j S b j · ˙ j
444 443 r19.29an φ a B S finSupp 0 ˙ a X = R a k S a k k b B S finSupp 0 ˙ b X = R j S b j · ˙ j
445 291 444 impbida φ b B S finSupp 0 ˙ b X = R j S b j · ˙ j a B S finSupp 0 ˙ a X = R a k S a k k
446 14 445 bitrd φ X N S a B S finSupp 0 ˙ a X = R a k S a k k