Metamath Proof Explorer


Theorem dvmptfprodlem

Description: Induction step for dvmptfprod . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptfprodlem.xph x φ
dvmptfprodlem.iph i φ
dvmptfprodlem.jph j φ
dvmptfprodlem.if _ i F
dvmptfprodlem.jg _ j G
dvmptfprodlem.a φ i I x X A
dvmptfprodlem.d φ D Fin
dvmptfprodlem.e φ E V
dvmptfprodlem.db φ ¬ E D
dvmptfprodlem.ss φ D E I
dvmptfprodlem.s φ S
dvmptfprodlem.c φ x X j D C
dvmptfprodlem.dvp φ dx X i D A dS x = x X j D C i D j A
dvmptfprodlem.14 φ x X G
dvmptfprodlem.dvf φ dx X F dS x = x X G
dvmptfprodlem.f i = E A = F
dvmptfprodlem.cg j = E C = G
Assertion dvmptfprodlem φ dx X i D E A dS x = x X j D E C i D E j A

Proof

Step Hyp Ref Expression
1 dvmptfprodlem.xph x φ
2 dvmptfprodlem.iph i φ
3 dvmptfprodlem.jph j φ
4 dvmptfprodlem.if _ i F
5 dvmptfprodlem.jg _ j G
6 dvmptfprodlem.a φ i I x X A
7 dvmptfprodlem.d φ D Fin
8 dvmptfprodlem.e φ E V
9 dvmptfprodlem.db φ ¬ E D
10 dvmptfprodlem.ss φ D E I
11 dvmptfprodlem.s φ S
12 dvmptfprodlem.c φ x X j D C
13 dvmptfprodlem.dvp φ dx X i D A dS x = x X j D C i D j A
14 dvmptfprodlem.14 φ x X G
15 dvmptfprodlem.dvf φ dx X F dS x = x X G
16 dvmptfprodlem.f i = E A = F
17 dvmptfprodlem.cg j = E C = G
18 nfcv _ i x
19 nfcv _ i X
20 18 19 nfel i x X
21 2 20 nfan i φ x X
22 4 a1i φ x X _ i F
23 snfi E Fin
24 23 a1i φ E Fin
25 unfi D Fin E Fin D E Fin
26 7 24 25 syl2anc φ D E Fin
27 26 adantr φ x X D E Fin
28 simpll φ x X i D E φ
29 10 sselda φ i D E i I
30 29 adantlr φ x X i D E i I
31 simplr φ x X i D E x X
32 28 30 31 6 syl3anc φ x X i D E A
33 snidg E V E E
34 8 33 syl φ E E
35 elun2 E E E D E
36 34 35 syl φ E D E
37 36 adantr φ x X E D E
38 16 adantl φ x X i = E A = F
39 21 22 27 32 37 38 fprodsplit1f φ x X i D E A = F i D E E A
40 difundir D E E = D E E E
41 40 a1i φ D E E = D E E E
42 difsn ¬ E D D E = D
43 9 42 syl φ D E = D
44 difid E E =
45 44 a1i φ E E =
46 43 45 uneq12d φ D E E E = D
47 un0 D = D
48 47 a1i φ D = D
49 41 46 48 3eqtrd φ D E E = D
50 49 prodeq1d φ i D E E A = i D A
51 50 oveq2d φ F i D E E A = F i D A
52 51 adantr φ x X F i D E E A = F i D A
53 39 52 eqtrd φ x X i D E A = F i D A
54 1 53 mpteq2da φ x X i D E A = x X F i D A
55 54 oveq2d φ dx X i D E A dS x = dx X F i D A dS x
56 10 36 sseldd φ E I
57 56 adantr φ x X E I
58 simpl φ x X φ
59 simpr φ x X x X
60 58 57 59 3jca φ x X φ E I x X
61 nfcv _ i E
62 nfv i E I
63 2 62 20 nf3an i φ E I x X
64 nfcv _ i
65 4 64 nfel i F
66 63 65 nfim i φ E I x X F
67 ancom φ x X i = E i = E φ x X
68 67 imbi1i φ x X i = E A = F i = E φ x X A = F
69 eqcom A = F F = A
70 69 imbi2i i = E φ x X A = F i = E φ x X F = A
71 68 70 bitri φ x X i = E A = F i = E φ x X F = A
72 38 71 mpbi i = E φ x X F = A
73 72 3adantr2 i = E φ E I x X F = A
74 73 3adant2 i = E φ i I x X A φ E I x X F = A
75 simp3 i = E φ i I x X A φ E I x X φ E I x X
76 eleq1 i = E i I E I
77 76 3anbi2d i = E φ i I x X φ E I x X
78 77 imbi1d i = E φ i I x X A φ E I x X A
79 78 biimpa i = E φ i I x X A φ E I x X A
80 79 3adant3 i = E φ i I x X A φ E I x X φ E I x X A
81 75 80 mpd i = E φ i I x X A φ E I x X A
82 74 81 eqeltrd i = E φ i I x X A φ E I x X F
83 82 3exp i = E φ i I x X A φ E I x X F
84 6 2a1i i = E φ E I x X F φ i I x X A
85 83 84 impbid i = E φ i I x X A φ E I x X F
86 61 66 85 6 vtoclgf E I φ E I x X F
87 57 60 86 sylc φ x X F
88 58 7 syl φ x X D Fin
89 58 adantr φ x X i D φ
90 10 adantr φ i D D E I
91 elun1 i D i D E
92 91 adantl φ i D i D E
93 90 92 sseldd φ i D i I
94 93 adantlr φ x X i D i I
95 59 adantr φ x X i D x X
96 89 94 95 6 syl3anc φ x X i D A
97 21 88 96 fprodclf φ x X i D A
98 nfv j x X
99 3 98 nfan j φ x X
100 diffi D Fin D j Fin
101 7 100 syl φ D j Fin
102 101 adantr φ x X D j Fin
103 eldifi i D j i D
104 103 adantl φ x X i D j i D
105 104 96 syldan φ x X i D j A
106 21 102 105 fprodclf φ x X i D j A
107 106 adantr φ x X j D i D j A
108 12 107 mulcld φ x X j D C i D j A
109 99 88 108 fsumclf φ x X j D C i D j A
110 1 11 87 14 15 97 109 13 dvmptmulf φ dx X F i D A dS x = x X G i D A + j D C i D j A F
111 nfcv _ j ×
112 nfcv _ j i D E E A
113 5 111 112 nfov _ j G i D E E A
114 58 8 syl φ x X E V
115 58 9 syl φ x X ¬ E D
116 diffi D E Fin D E j Fin
117 26 116 syl φ D E j Fin
118 117 adantr φ x X D E j Fin
119 eldifi i D E j i D E
120 119 adantl φ x X i D E j i D E
121 120 32 syldan φ x X i D E j A
122 21 118 121 fprodclf φ x X i D E j A
123 122 adantr φ x X j D i D E j A
124 12 123 mulcld φ x X j D C i D E j A
125 sneq j = E j = E
126 125 difeq2d j = E D E j = D E E
127 126 prodeq1d j = E i D E j A = i D E E A
128 17 127 oveq12d j = E C i D E j A = G i D E E A
129 49 7 eqeltrd φ D E E Fin
130 129 adantr φ x X D E E Fin
131 58 adantr φ x X i D E E φ
132 10 adantr φ i D E E D E I
133 eldifi i D E E i D E
134 133 adantl φ i D E E i D E
135 132 134 sseldd φ i D E E i I
136 135 adantlr φ x X i D E E i I
137 59 adantr φ x X i D E E x X
138 131 136 137 6 syl3anc φ x X i D E E A
139 21 130 138 fprodclf φ x X i D E E A
140 14 139 mulcld φ x X G i D E E A
141 99 113 88 114 115 124 128 140 fsumsplitsn φ x X j D E C i D E j A = j D C i D E j A + G i D E E A
142 difundir D E j = D j E j
143 142 a1i φ j D D E j = D j E j
144 nfv x j D
145 1 144 nfan x φ j D
146 elsni x E x = E
147 146 eqcomd x E E = x
148 147 adantr x E x = j E = x
149 simpr x E x = j x = j
150 eqidd x E x = j j = j
151 148 149 150 3eqtrd x E x = j E = j
152 151 adantll φ j D x E x = j E = j
153 simpllr φ j D x E x = j j D
154 152 153 eqeltrd φ j D x E x = j E D
155 9 ad3antrrr φ j D x E x = j ¬ E D
156 154 155 pm2.65da φ j D x E ¬ x = j
157 velsn x j x = j
158 156 157 sylnibr φ j D x E ¬ x j
159 158 ex φ j D x E ¬ x j
160 145 159 ralrimi φ j D x E ¬ x j
161 disj E j = x E ¬ x j
162 160 161 sylibr φ j D E j =
163 disjdif2 E j = E j = E
164 162 163 syl φ j D E j = E
165 164 uneq2d φ j D D j E j = D j E
166 143 165 eqtrd φ j D D E j = D j E
167 166 prodeq1d φ j D i D E j A = i D j E A
168 167 adantlr φ x X j D i D E j A = i D j E A
169 nfv i j D
170 21 169 nfan i φ x X j D
171 102 adantr φ x X j D D j Fin
172 58 adantr φ x X j D φ
173 172 8 syl φ x X j D E V
174 id ¬ E D ¬ E D
175 174 intnanrd ¬ E D ¬ E D ¬ E j
176 174 175 syl ¬ E D ¬ E D ¬ E j
177 eldif E D j E D ¬ E j
178 176 177 sylnibr ¬ E D ¬ E D j
179 9 178 syl φ ¬ E D j
180 172 179 syl φ x X j D ¬ E D j
181 105 adantlr φ x X j D i D j A
182 87 adantr φ x X j D F
183 170 4 171 173 180 181 16 182 fprodsplitsn φ x X j D i D j E A = i D j A F
184 eqidd φ x X j D i D j A F = i D j A F
185 168 183 184 3eqtrd φ x X j D i D E j A = i D j A F
186 185 oveq2d φ x X j D C i D E j A = C i D j A F
187 12 107 182 mulassd φ x X j D C i D j A F = C i D j A F
188 187 eqcomd φ x X j D C i D j A F = C i D j A F
189 186 188 eqtrd φ x X j D C i D E j A = C i D j A F
190 189 ex φ x X j D C i D E j A = C i D j A F
191 99 190 ralrimi φ x X j D C i D E j A = C i D j A F
192 191 sumeq2d φ x X j D C i D E j A = j D C i D j A F
193 99 88 87 108 fsummulc1f φ x X j D C i D j A F = j D C i D j A F
194 193 eqcomd φ x X j D C i D j A F = j D C i D j A F
195 eqidd φ x X j D C i D j A F = j D C i D j A F
196 192 194 195 3eqtrd φ x X j D C i D E j A = j D C i D j A F
197 109 87 mulcld φ x X j D C i D j A F
198 196 197 eqeltrd φ x X j D C i D E j A
199 198 140 addcomd φ x X j D C i D E j A + G i D E E A = G i D E E A + j D C i D E j A
200 50 oveq2d φ G i D E E A = G i D A
201 200 adantr φ x X G i D E E A = G i D A
202 201 196 oveq12d φ x X G i D E E A + j D C i D E j A = G i D A + j D C i D j A F
203 141 199 202 3eqtrrd φ x X G i D A + j D C i D j A F = j D E C i D E j A
204 1 203 mpteq2da φ x X G i D A + j D C i D j A F = x X j D E C i D E j A
205 55 110 204 3eqtrd φ dx X i D E A dS x = x X j D E C i D E j A