Step | Hyp | Ref
| Expression |
1 | | hoidmvle.s |
. 2
|
2 | | hoidmvle.d |
. . . 4
|
3 | | ovex 6678 |
. . . . . . 7
|
4 | | nnex 11026 |
. . . . . . 7
|
5 | 3, 4 | pm3.2i 471 |
. . . . . 6
|
6 | 5 | a1i 11 |
. . . . 5
|
7 | | elmapg 7870 |
. . . . 5
|
8 | 6, 7 | syl 17 |
. . . 4
|
9 | 2, 8 | mpbird 247 |
. . 3
|
10 | | hoidmvle.c |
. . . . 5
|
11 | | elmapg 7870 |
. . . . . 6
|
12 | 6, 11 | syl 17 |
. . . . 5
|
13 | 10, 12 | mpbird 247 |
. . . 4
|
14 | | hoidmvle.b |
. . . . . 6
|
15 | | reex 10027 |
. . . . . . . . 9
|
16 | 15 | a1i 11 |
. . . . . . . 8
|
17 | | hoidmvle.x |
. . . . . . . 8
|
18 | 16, 17 | jca 554 |
. . . . . . 7
|
19 | | elmapg 7870 |
. . . . . . 7
|
20 | 18, 19 | syl 17 |
. . . . . 6
|
21 | 14, 20 | mpbird 247 |
. . . . 5
|
22 | | hoidmvle.a |
. . . . . . 7
|
23 | | elmapg 7870 |
. . . . . . . 8
|
24 | 18, 23 | syl 17 |
. . . . . . 7
|
25 | 22, 24 | mpbird 247 |
. . . . . 6
|
26 | | oveq2 6658 |
. . . . . . . . . 10
|
27 | 26 | eleq2d 2687 |
. . . . . . . . 9
|
28 | 26 | eleq2d 2687 |
. . . . . . . . . . 11
|
29 | 26 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
30 | 29 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
31 | 29 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
32 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . 17
|
33 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . . 18
|
34 | 33 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . 17
|
35 | 32, 34 | sseq12d 3634 |
. . . . . . . . . . . . . . . 16
|
36 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
38 | 36 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 38 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
41 | 37, 40 | breq12d 4666 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
42 | 35, 41 | imbi12d 334 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
43 | 31, 42 | imbi12d 334 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
44 | 43 | ralbidv2 2984 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
45 | 30, 44 | imbi12d 334 |
. . . . . . . . . . . 12
Σ^
Σ^ |
46 | 45 | ralbidv2 2984 |
. . . . . . . . . . 11
Σ^
Σ^ |
47 | 28, 46 | imbi12d 334 |
. . . . . . . . . 10
Σ^
Σ^ |
48 | 47 | ralbidv2 2984 |
. . . . . . . . 9
Σ^
Σ^ |
49 | 27, 48 | imbi12d 334 |
. . . . . . . 8
Σ^
Σ^ |
50 | 49 | ralbidv2 2984 |
. . . . . . 7
Σ^
Σ^ |
51 | | oveq2 6658 |
. . . . . . . . . 10
|
52 | 51 | eleq2d 2687 |
. . . . . . . . 9
|
53 | 51 | eleq2d 2687 |
. . . . . . . . . . 11
|
54 | 51 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
55 | 54 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
56 | 54 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
57 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . 17
|
58 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . 17
|
60 | 57, 59 | sseq12d 3634 |
. . . . . . . . . . . . . . . 16
|
61 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
63 | 61 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
66 | 62, 65 | breq12d 4666 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
67 | 60, 66 | imbi12d 334 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
68 | 56, 67 | imbi12d 334 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
69 | 68 | ralbidv2 2984 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
70 | 55, 69 | imbi12d 334 |
. . . . . . . . . . . 12
Σ^
Σ^ |
71 | 70 | ralbidv2 2984 |
. . . . . . . . . . 11
Σ^
Σ^ |
72 | 53, 71 | imbi12d 334 |
. . . . . . . . . 10
Σ^
Σ^ |
73 | 72 | ralbidv2 2984 |
. . . . . . . . 9
Σ^
Σ^ |
74 | 52, 73 | imbi12d 334 |
. . . . . . . 8
Σ^
Σ^ |
75 | 74 | ralbidv2 2984 |
. . . . . . 7
Σ^
Σ^ |
76 | | oveq2 6658 |
. . . . . . . . . 10
|
77 | 76 | eleq2d 2687 |
. . . . . . . . 9
|
78 | 76 | eleq2d 2687 |
. . . . . . . . . . 11
|
79 | 76 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
80 | 79 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
81 | 79 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
82 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . 17
|
83 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . 17
|
85 | 82, 84 | sseq12d 3634 |
. . . . . . . . . . . . . . . 16
|
86 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
87 | 86 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
88 | 86 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 88 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
90 | 89 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
91 | 87, 90 | breq12d 4666 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
92 | 85, 91 | imbi12d 334 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
93 | 81, 92 | imbi12d 334 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
94 | 93 | ralbidv2 2984 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
95 | 80, 94 | imbi12d 334 |
. . . . . . . . . . . 12
Σ^
Σ^ |
96 | 95 | ralbidv2 2984 |
. . . . . . . . . . 11
Σ^
Σ^ |
97 | 78, 96 | imbi12d 334 |
. . . . . . . . . 10
Σ^
Σ^ |
98 | 97 | ralbidv2 2984 |
. . . . . . . . 9
Σ^
Σ^ |
99 | 77, 98 | imbi12d 334 |
. . . . . . . 8
Σ^
Σ^ |
100 | 99 | ralbidv2 2984 |
. . . . . . 7
Σ^
Σ^ |
101 | | oveq2 6658 |
. . . . . . . . . 10
|
102 | 101 | eleq2d 2687 |
. . . . . . . . 9
|
103 | 101 | eleq2d 2687 |
. . . . . . . . . . 11
|
104 | 101 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
105 | 104 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
106 | 104 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
107 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . 17
|
108 | | ixpeq1 7919 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . 17
|
110 | 107, 109 | sseq12d 3634 |
. . . . . . . . . . . . . . . 16
|
111 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
113 | 111 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
116 | 112, 115 | breq12d 4666 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
117 | 110, 116 | imbi12d 334 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
118 | 106, 117 | imbi12d 334 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
119 | 118 | ralbidv2 2984 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
120 | 105, 119 | imbi12d 334 |
. . . . . . . . . . . 12
Σ^
Σ^ |
121 | 120 | ralbidv2 2984 |
. . . . . . . . . . 11
Σ^
Σ^ |
122 | 103, 121 | imbi12d 334 |
. . . . . . . . . 10
Σ^
Σ^ |
123 | 122 | ralbidv2 2984 |
. . . . . . . . 9
Σ^
Σ^ |
124 | 102, 123 | imbi12d 334 |
. . . . . . . 8
Σ^
Σ^ |
125 | 124 | ralbidv2 2984 |
. . . . . . 7
Σ^
Σ^ |
126 | | hoidmvle.l |
. . . . . . . . . . . . . . . 16
|
127 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
128 | 127 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
|
129 | 128 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
130 | 129 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . . . . 19
|
131 | 130 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . 18
|
132 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
|
133 | 132 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | 133 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 134 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . . . . 19
|
136 | 135 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . 18
|
137 | 131, 136 | cbvmpt2v 6735 |
. . . . . . . . . . . . . . . . 17
|
138 | 137 | mpteq2i 4741 |
. . . . . . . . . . . . . . . 16
|
139 | 126, 138 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
140 | | elmapi 7879 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . 15
|
142 | | elmapi 7879 |
. . . . . . . . . . . . . . . 16
|
143 | 142 | adantl 482 |
. . . . . . . . . . . . . . 15
|
144 | 139, 141,
143 | hoidmv0val 40797 |
. . . . . . . . . . . . . 14
|
145 | 144 | ad5ant23 1304 |
. . . . . . . . . . . . 13
|
146 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
147 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
|
148 | | icossicc 12260 |
. . . . . . . . . . . . . . . 16
|
149 | | 0fin 8188 |
. . . . . . . . . . . . . . . . . 18
|
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
151 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . . 20
|
152 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
155 | 151, 152,
153, 154 | fvmap 39387 |
. . . . . . . . . . . . . . . . . . 19
|
156 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
158 | 157 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
159 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . . 20
|
160 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
162 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
163 | 159, 160,
161, 162 | fvmap 39387 |
. . . . . . . . . . . . . . . . . . 19
|
164 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
166 | 165 | adantll 750 |
. . . . . . . . . . . . . . . . 17
|
167 | 126, 150,
158, 166 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . 16
|
168 | 148, 167 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
169 | 146, 147,
168 | sge0ge0mpt 40655 |
. . . . . . . . . . . . . 14
Σ^ |
170 | 169 | adantll 750 |
. . . . . . . . . . . . 13
Σ^ |
171 | 145, 170 | eqbrtrd 4675 |
. . . . . . . . . . . 12
Σ^ |
172 | 171 | a1d 25 |
. . . . . . . . . . 11
Σ^ |
173 | 172 | ralrimiva 2966 |
. . . . . . . . . 10
Σ^ |
174 | 173 | ralrimiva 2966 |
. . . . . . . . 9
Σ^ |
175 | 174 | ralrimiva 2966 |
. . . . . . . 8
Σ^ |
176 | 175 | ralrimiva 2966 |
. . . . . . 7
Σ^ |
177 | | simpl 473 |
. . . . . . . . 9
Σ^
|
178 | 128 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . 18
|
179 | 178 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
|
180 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
181 | 180 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
Σ^
Σ^ |
182 | 179, 181 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
183 | 182 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
184 | 183 | ralbidv 2986 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
185 | 184 | ralbidv 2986 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
186 | 133 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . 20
|
187 | 186 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . 19
|
188 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
189 | 188 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
Σ^
Σ^ |
190 | 187, 189 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
Σ^
Σ^ |
191 | 190 | ralbidv 2986 |
. . . . . . . . . . . . . . . . 17
Σ^
Σ^ |
192 | 191 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
193 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
194 | 193 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
195 | 194 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
196 | 195 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
197 | 196 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
198 | 197 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . . . . . . . 22
|
199 | 198 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . 21
|
200 | 193 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
201 | 200 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
202 | 201 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
Σ^ Σ^ |
203 | 202 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
Σ^
Σ^ |
204 | 199, 203 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
Σ^ |
205 | 204 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . 19
Σ^
Σ^ |
206 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
207 | 206 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
208 | 207 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
209 | 208 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
210 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
211 | 210 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
212 | 211 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . . 22
|
213 | 206 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
214 | 213 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
215 | 214 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
Σ^ Σ^ |
216 | 215 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . 22
Σ^
Σ^ |
217 | 212, 216 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . 21
Σ^
Σ^ |
218 | 217 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
Σ^ |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Σ^
Σ^ |
220 | 205, 219 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
Σ^
Σ^ |
221 | 220 | cbvralv 3171 |
. . . . . . . . . . . . . . . . 17
Σ^
Σ^ |
222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
223 | 192, 222 | bitrd 268 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
224 | 223 | cbvralv 3171 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
225 | 224 | a1i 11 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
226 | 185, 225 | bitrd 268 |
. . . . . . . . . . . 12
Σ^
Σ^ |
227 | 226 | cbvralv 3171 |
. . . . . . . . . . 11
Σ^
Σ^ |
228 | 227 | biimpi 206 |
. . . . . . . . . 10
Σ^
Σ^ |
229 | 228 | adantl 482 |
. . . . . . . . 9
Σ^
Σ^ |
230 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
231 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
232 | 231 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
233 | 232 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
234 | 233 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
235 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
236 | | uneq1 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
237 | | 0un 39215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
239 | 236, 238 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
240 | 239 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
241 | 240 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
242 | 241 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
243 | 235, 242 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
244 | 243 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
245 | 230, 234,
244 | jca31 557 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
246 | 245 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . 22
Σ^ |
247 | 246 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
Σ^
|
248 | 247 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
|
249 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
250 | 241 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
251 | 249, 250 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . 22
|
252 | 251 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
253 | 252 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
|
254 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
|
255 | 241 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
256 | 255 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
257 | 254, 256 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . 21
|
258 | 257 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
|
259 | 248, 253,
258 | jca31 557 |
. . . . . . . . . . . . . . . . . . 19
Σ^
|
260 | 259 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
261 | 260 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
Σ^
|
262 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
263 | 255 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
264 | 262, 263 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
|
265 | 264 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
266 | 265 | adantlll 754 |
. . . . . . . . . . . . . . . . 17
Σ^
|
267 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
268 | 239 | ixpeq1d 7920 |
. . . . . . . . . . . . . . . . . . . . 21
|
269 | 268 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
270 | 239 | ixpeq1d 7920 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
271 | 270 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
272 | 271 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . . . . . . . 22
|
273 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
274 | 273 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
275 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
276 | 275 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
277 | 274, 276 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
278 | 277 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
279 | 278 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
280 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
281 | 272, 280 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
282 | 281 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
283 | 269, 282 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . 19
|
284 | 267, 283 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
285 | 284 | adantll 750 |
. . . . . . . . . . . . . . . . 17
Σ^
|
286 | 261, 266,
285 | jca31 557 |
. . . . . . . . . . . . . . . 16
Σ^
|
287 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Σ^
|
288 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
289 | 288 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
290 | 289 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
291 | 290 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
292 | 291 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . . . . . 22
|
293 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
294 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
295 | 293, 294 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
296 | 295 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
297 | 296 | cbvprodv 14646 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
298 | 297 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
299 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
300 | 299 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
301 | 300 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
302 | 301 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
303 | 298, 302 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
304 | 303 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . . . . . 22
|
305 | 292, 304 | cbvmpt2v 6735 |
. . . . . . . . . . . . . . . . . . . . 21
|
306 | 305 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . . . . 20
|
307 | 126, 306 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
308 | | simp-6r 811 |
. . . . . . . . . . . . . . . . . . 19
|
309 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
310 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
|
311 | 310 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
312 | 311 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
313 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
|
314 | 313 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
315 | 314 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
316 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
|
317 | 316 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
318 | 317 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
319 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
|
320 | 319 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
321 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
322 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
323 | 322, 294 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
324 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
325 | 324 | imbi1i 339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
326 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
327 | 326 | imbi2i 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
328 | 325, 327 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
329 | 323, 328 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
330 | 329 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
331 | 330 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
332 | 277 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
333 | 332 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
334 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
335 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
336 | 334, 335 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
337 | 336 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
338 | 337 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
339 | 338 | iuneq2i 4539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
340 | 333, 339 | eqtr2i 2645 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
341 | 340 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
342 | 331, 341 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . . . 21
|
343 | 321, 342 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
|
344 | 343 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
345 | 307, 308,
309, 312, 315, 318, 320, 344 | hoidmv1le 40808 |
. . . . . . . . . . . . . . . . . 18
Σ^ |
346 | 345 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Σ^ |
347 | 236, 238 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
348 | 347 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
349 | 348 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
350 | 349 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
351 | 348 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . . . 21
|
352 | 351 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . 20
|
353 | 352 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
Σ^ Σ^ |
354 | 353 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Σ^ Σ^ |
355 | 350, 354 | breq12d 4666 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
356 | 346, 355 | mpbird 247 |
. . . . . . . . . . . . . . . 16
Σ^ |
357 | 286, 287,
356 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
358 | 17 | ad8antr 776 |
. . . . . . . . . . . . . . . . 17
Σ^
|
359 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
Σ^
|
360 | 359 | ad5ant12 1300 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
361 | 360 | ad5ant12 1300 |
. . . . . . . . . . . . . . . . 17
Σ^
|
362 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
Σ^
|
363 | 362 | ad5ant12 1300 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
364 | 363 | ad5ant12 1300 |
. . . . . . . . . . . . . . . . 17
Σ^
|
365 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
366 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
|
367 | 366 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
368 | 367 | ad4ant23 1297 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
369 | 368 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
Σ^
|
370 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
|
371 | 370 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
372 | 371 | ad4ant23 1297 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
373 | 372 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
Σ^
|
374 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
375 | 374 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Σ^
|
376 | 375 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
Σ^
|
377 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
378 | 377 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
379 | 378 | adantlll 754 |
. . . . . . . . . . . . . . . . 17
Σ^
|
380 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
381 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
382 | 380, 381 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
383 | 382 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
384 | 383 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
385 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
386 | 385 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
387 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
388 | 387 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
389 | 386, 388 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
390 | 389 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
391 | 390 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
392 | 391 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
393 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
394 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
395 | 393, 394 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
396 | 395 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
397 | 396 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
398 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
399 | 398 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
400 | 399 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
401 | 400 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
402 | 397, 401 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
403 | 402 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
404 | 403 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
405 | 392, 404 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
406 | 384, 405 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
407 | 385, 387 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
408 | 407 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
409 | 408 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
410 | 398 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
411 | 410 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
412 | 409, 411 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
413 | 412 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Σ^ Σ^ |
414 | 413 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Σ^
Σ^ |
415 | 406, 414 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Σ^
Σ^ |
416 | 415 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . . . . 23
Σ^
Σ^ |
417 | 416 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . . 22
Σ^
Σ^ |
418 | 417 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . 21
Σ^
Σ^ |
419 | 418 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . 20
Σ^
Σ^ |
420 | 419 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
Σ^
Σ^ |
421 | 420 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Σ^
Σ^ |
422 | 421 | ad6antr 772 |
. . . . . . . . . . . . . . . . 17
Σ^
Σ^ |
423 | 323 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . 20
|
424 | 336 | cbvixpv 7926 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
425 | 424 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
426 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
427 | 426 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
428 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
429 | 428 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
430 | 427, 429 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
431 | 430 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . . . . . 22
|
432 | 425, 431 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
433 | 432 | cbviunv 4559 |
. . . . . . . . . . . . . . . . . . . 20
|
434 | 423, 433 | sseq12i 3631 |
. . . . . . . . . . . . . . . . . . 19
|
435 | 434 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
436 | 435 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
Σ^
|
437 | | neqne 2802 |
. . . . . . . . . . . . . . . . . 18
|
438 | 437 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Σ^
|
439 | 307, 358,
361, 364, 365, 369, 373, 376, 379, 422, 436, 438 | hoidmvlelem5 40813 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^ |
440 | 273, 275 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
441 | 440 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . 18
|
442 | 441 | fveq2i 6194 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
443 | 442 | breq2i 4661 |
. . . . . . . . . . . . . . . 16
Σ^ Σ^ |
444 | 439, 443 | sylib 208 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
445 | 357, 444 | pm2.61dan 832 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
446 | 445 | ex 450 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
447 | 446 | ralrimiva 2966 |
. . . . . . . . . . . 12
Σ^
Σ^ |
448 | 447 | ralrimiva 2966 |
. . . . . . . . . . 11
Σ^
Σ^ |
449 | 448 | ralrimiva 2966 |
. . . . . . . . . 10
Σ^
Σ^ |
450 | 449 | ralrimiva 2966 |
. . . . . . . . 9
Σ^
Σ^ |
451 | 177, 229,
450 | syl2anc 693 |
. . . . . . . 8
Σ^
Σ^ |
452 | 451 | ex 450 |
. . . . . . 7
Σ^
Σ^ |
453 | 50, 75, 100, 125, 176, 452, 17 | findcard2d 8202 |
. . . . . 6
Σ^ |
454 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
455 | 454 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
456 | 455 | ixpeq2dv 7924 |
. . . . . . . . . . . 12
|
457 | 456 | sseq1d 3632 |
. . . . . . . . . . 11
|
458 | | oveq1 6657 |
. . . . . . . . . . . 12
|
459 | 458 | breq1d 4663 |
. . . . . . . . . . 11
Σ^
Σ^ |
460 | 457, 459 | imbi12d 334 |
. . . . . . . . . 10
Σ^
Σ^ |
461 | 460 | ralbidv 2986 |
. . . . . . . . 9
Σ^
Σ^ |
462 | 461 | ralbidv 2986 |
. . . . . . . 8
Σ^
Σ^ |
463 | 462 | ralbidv 2986 |
. . . . . . 7
Σ^
Σ^ |
464 | 463 | rspcva 3307 |
. . . . . 6
Σ^
Σ^ |
465 | 25, 453, 464 | syl2anc 693 |
. . . . 5
Σ^ |
466 | | fveq1 6190 |
. . . . . . . . . . . 12
|
467 | 466 | oveq2d 6666 |
. . . . . . . . . . 11
|
468 | 467 | ixpeq2dv 7924 |
. . . . . . . . . 10
|
469 | 468 | sseq1d 3632 |
. . . . . . . . 9
|
470 | | oveq2 6658 |
. . . . . . . . . 10
|
471 | 470 | breq1d 4663 |
. . . . . . . . 9
Σ^
Σ^ |
472 | 469, 471 | imbi12d 334 |
. . . . . . . 8
Σ^
Σ^ |
473 | 472 | ralbidv 2986 |
. . . . . . 7
Σ^
Σ^ |
474 | 473 | ralbidv 2986 |
. . . . . 6
Σ^
Σ^ |
475 | 474 | rspcva 3307 |
. . . . 5
Σ^
Σ^ |
476 | 21, 465, 475 | syl2anc 693 |
. . . 4
Σ^ |
477 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
478 | 477 | fveq1d 6193 |
. . . . . . . . . . . 12
|
479 | 478 | oveq1d 6665 |
. . . . . . . . . . 11
|
480 | 479 | ixpeq2dv 7924 |
. . . . . . . . . 10
|
481 | 480 | adantr 481 |
. . . . . . . . 9
|
482 | 481 | iuneq2dv 4542 |
. . . . . . . 8
|
483 | 482 | sseq2d 3633 |
. . . . . . 7
|
484 | 477 | oveq1d 6665 |
. . . . . . . . . 10
|
485 | 484 | mpteq2dv 4745 |
. . . . . . . . 9
|
486 | 485 | fveq2d 6195 |
. . . . . . . 8
Σ^ Σ^ |
487 | 486 | breq2d 4665 |
. . . . . . 7
Σ^
Σ^ |
488 | 483, 487 | imbi12d 334 |
. . . . . 6
Σ^
Σ^ |
489 | 488 | ralbidv 2986 |
. . . . 5
Σ^
Σ^ |
490 | 489 | rspcva 3307 |
. . . 4
Σ^
Σ^ |
491 | 13, 476, 490 | syl2anc 693 |
. . 3
Σ^ |
492 | | fveq1 6190 |
. . . . . . . . . . 11
|
493 | 492 | fveq1d 6193 |
. . . . . . . . . 10
|
494 | 493 | oveq2d 6666 |
. . . . . . . . 9
|
495 | 494 | ixpeq2dv 7924 |
. . . . . . . 8
|
496 | 495 | adantr 481 |
. . . . . . 7
|
497 | 496 | iuneq2dv 4542 |
. . . . . 6
|
498 | 497 | sseq2d 3633 |
. . . . 5
|
499 | 492 | oveq2d 6666 |
. . . . . . . 8
|
500 | 499 | mpteq2dv 4745 |
. . . . . . 7
|
501 | 500 | fveq2d 6195 |
. . . . . 6
Σ^ Σ^ |
502 | 501 | breq2d 4665 |
. . . . 5
Σ^
Σ^ |
503 | 498, 502 | imbi12d 334 |
. . . 4
Σ^
Σ^ |
504 | 503 | rspcva 3307 |
. . 3
Σ^
Σ^ |
505 | 9, 491, 504 | syl2anc 693 |
. 2
Σ^ |
506 | 1, 505 | mpd 15 |
1
Σ^ |