Proof of Theorem ovncvr2
Step | Hyp | Ref
| Expression |
1 | | ovncvr2.c |
. . . . . . . . . . . . . . . . 17
|
2 | 1 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
3 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . 18
|
4 | 3 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
|
5 | 4 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
6 | | ovncvr2.a |
. . . . . . . . . . . . . . . . 17
|
7 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . 19
|
8 | 7, 6 | ssexd 4805 |
. . . . . . . . . . . . . . . . . 18
|
9 | | elpwg 4166 |
. . . . . . . . . . . . . . . . . 18
|
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
11 | 6, 10 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
12 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
|
13 | 12 | rabex 4813 |
. . . . . . . . . . . . . . . . 17
|
14 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
15 | 2, 5, 11, 14 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
16 | | ssrab2 3687 |
. . . . . . . . . . . . . . . 16
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
|
18 | 15, 17 | eqsstrd 3639 |
. . . . . . . . . . . . . 14
|
19 | | ovncvr2.i |
. . . . . . . . . . . . . . . . 17
|
20 | | ovncvr2.d |
. . . . . . . . . . . . . . . . . . . 20
Σ^ voln* |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Σ^ voln* |
22 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
23 | 22 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
voln* voln* |
25 | 24 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . 24
voln* voln* |
26 | 25 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . 23
Σ^ voln* Σ^ voln* |
27 | 23, 26 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
Σ^ voln*
Σ^ voln* |
28 | 27 | rabbidva2 3186 |
. . . . . . . . . . . . . . . . . . . . 21
Σ^ voln* Σ^ voln* |
29 | 28 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . 20
Σ^ voln* Σ^ voln* |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Σ^ voln* Σ^ voln* |
31 | | rpex 39562 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 31 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . 20
Σ^ voln* |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Σ^ voln* |
34 | 21, 30, 11, 33 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . 18
Σ^ voln* |
35 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
voln* voln* |
36 | 35 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . 20
Σ^ voln* Σ^ voln* |
37 | 36 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . 19
Σ^ voln* Σ^ voln* |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Σ^ voln* Σ^ voln* |
39 | | ovncvr2.e |
. . . . . . . . . . . . . . . . . 18
|
40 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | rabex 4813 |
. . . . . . . . . . . . . . . . . . 19
Σ^ voln* |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
Σ^ voln* |
43 | 34, 38, 39, 42 | fvmptd 6288 |
. . . . . . . . . . . . . . . . 17
Σ^ voln* |
44 | 19, 43 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
Σ^ voln* |
45 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | 45 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 47 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
Σ^ Σ^ |
49 | 48 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
Σ^ voln* Σ^ voln* |
50 | 49 | elrab 3363 |
. . . . . . . . . . . . . . . 16
Σ^ voln*
Σ^ voln* |
51 | 44, 50 | sylib 208 |
. . . . . . . . . . . . . . 15
Σ^ voln* |
52 | 51 | simpld 475 |
. . . . . . . . . . . . . 14
|
53 | 18, 52 | sseldd 3604 |
. . . . . . . . . . . . 13
|
54 | | elmapi 7879 |
. . . . . . . . . . . . 13
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . 12
|
56 | 55 | adantr 481 |
. . . . . . . . . . 11
|
57 | | simpr 477 |
. . . . . . . . . . 11
|
58 | 56, 57 | ffvelrnd 6360 |
. . . . . . . . . 10
|
59 | | elmapi 7879 |
. . . . . . . . . 10
|
60 | 58, 59 | syl 17 |
. . . . . . . . 9
|
61 | 60 | ffvelrnda 6359 |
. . . . . . . 8
|
62 | | xp1st 7198 |
. . . . . . . 8
|
63 | 61, 62 | syl 17 |
. . . . . . 7
|
64 | | eqid 2622 |
. . . . . . 7
|
65 | 63, 64 | fmptd 6385 |
. . . . . 6
|
66 | | reex 10027 |
. . . . . . . . 9
|
67 | 66 | a1i 11 |
. . . . . . . 8
|
68 | | ovncvr2.x |
. . . . . . . 8
|
69 | | elmapg 7870 |
. . . . . . . 8
|
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . 7
|
71 | 70 | adantr 481 |
. . . . . 6
|
72 | 65, 71 | mpbird 247 |
. . . . 5
|
73 | | eqid 2622 |
. . . . 5
|
74 | 72, 73 | fmptd 6385 |
. . . 4
|
75 | | ovncvr2.b |
. . . . . 6
|
76 | 75 | a1i 11 |
. . . . 5
|
77 | 76 | feq1d 6030 |
. . . 4
|
78 | 74, 77 | mpbird 247 |
. . 3
|
79 | | xp2nd 7199 |
. . . . . . . 8
|
80 | 61, 79 | syl 17 |
. . . . . . 7
|
81 | | eqid 2622 |
. . . . . . 7
|
82 | 80, 81 | fmptd 6385 |
. . . . . 6
|
83 | | elmapg 7870 |
. . . . . . . 8
|
84 | 67, 68, 83 | syl2anc 693 |
. . . . . . 7
|
85 | 84 | adantr 481 |
. . . . . 6
|
86 | 82, 85 | mpbird 247 |
. . . . 5
|
87 | | eqid 2622 |
. . . . 5
|
88 | 86, 87 | fmptd 6385 |
. . . 4
|
89 | | ovncvr2.t |
. . . . . 6
|
90 | 89 | a1i 11 |
. . . . 5
|
91 | 90 | feq1d 6030 |
. . . 4
|
92 | 88, 91 | mpbird 247 |
. . 3
|
93 | 78, 92 | jca 554 |
. 2
|
94 | 15 | idi 2 |
. . . . . 6
|
95 | 52, 94 | eleqtrd 2703 |
. . . . 5
|
96 | | fveq1 6190 |
. . . . . . . . . . . 12
|
97 | 96 | coeq2d 5284 |
. . . . . . . . . . 11
|
98 | 97 | fveq1d 6193 |
. . . . . . . . . 10
|
99 | 98 | ixpeq2dv 7924 |
. . . . . . . . 9
|
100 | 99 | adantr 481 |
. . . . . . . 8
|
101 | 100 | iuneq2dv 4542 |
. . . . . . 7
|
102 | 101 | sseq2d 3633 |
. . . . . 6
|
103 | 102 | elrab 3363 |
. . . . 5
|
104 | 95, 103 | sylib 208 |
. . . 4
|
105 | 104 | simprd 479 |
. . 3
|
106 | 60 | adantr 481 |
. . . . . . 7
|
107 | | simpr 477 |
. . . . . . 7
|
108 | 106, 107 | fvovco 39381 |
. . . . . 6
|
109 | | mptexg 6484 |
. . . . . . . . . . . 12
|
110 | 68, 109 | syl 17 |
. . . . . . . . . . 11
|
111 | 110 | adantr 481 |
. . . . . . . . . 10
|
112 | 76, 111 | fvmpt2d 6293 |
. . . . . . . . 9
|
113 | | fvexd 6203 |
. . . . . . . . 9
|
114 | 112, 113 | fvmpt2d 6293 |
. . . . . . . 8
|
115 | 114 | eqcomd 2628 |
. . . . . . 7
|
116 | | mptexg 6484 |
. . . . . . . . . . . 12
|
117 | 68, 116 | syl 17 |
. . . . . . . . . . 11
|
118 | 117 | adantr 481 |
. . . . . . . . . 10
|
119 | 90, 118 | fvmpt2d 6293 |
. . . . . . . . 9
|
120 | | fvexd 6203 |
. . . . . . . . 9
|
121 | 119, 120 | fvmpt2d 6293 |
. . . . . . . 8
|
122 | 121 | eqcomd 2628 |
. . . . . . 7
|
123 | 115, 122 | oveq12d 6668 |
. . . . . 6
|
124 | 108, 123 | eqtrd 2656 |
. . . . 5
|
125 | 124 | ixpeq2dva 7923 |
. . . 4
|
126 | 125 | iuneq2dv 4542 |
. . 3
|
127 | 105, 126 | sseqtrd 3641 |
. 2
|
128 | | ovncvr2.l |
. . . . . . . 8
|
129 | 128 | a1i 11 |
. . . . . . 7
|
130 | | coeq2 5280 |
. . . . . . . . . . . . 13
|
131 | 130 | fveq1d 6193 |
. . . . . . . . . . . 12
|
132 | 131 | ad2antlr 763 |
. . . . . . . . . . 11
|
133 | 132 | adantllr 755 |
. . . . . . . . . 10
|
134 | 108 | adantlr 751 |
. . . . . . . . . 10
|
135 | 123 | adantlr 751 |
. . . . . . . . . 10
|
136 | 133, 134,
135 | 3eqtrd 2660 |
. . . . . . . . 9
|
137 | 136 | fveq2d 6195 |
. . . . . . . 8
|
138 | 137 | prodeq2dv 14653 |
. . . . . . 7
|
139 | 68 | adantr 481 |
. . . . . . . 8
|
140 | 75 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
141 | 57, 111, 140 | syl2anc 693 |
. . . . . . . . . . . . 13
|
142 | 141 | feq1d 6030 |
. . . . . . . . . . . 12
|
143 | 65, 142 | mpbird 247 |
. . . . . . . . . . 11
|
144 | 143 | adantr 481 |
. . . . . . . . . 10
|
145 | 144, 107 | ffvelrnd 6360 |
. . . . . . . . 9
|
146 | 89 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
147 | 57, 118, 146 | syl2anc 693 |
. . . . . . . . . . . . 13
|
148 | 147 | feq1d 6030 |
. . . . . . . . . . . 12
|
149 | 82, 148 | mpbird 247 |
. . . . . . . . . . 11
|
150 | 149 | adantr 481 |
. . . . . . . . . 10
|
151 | 150, 107 | ffvelrnd 6360 |
. . . . . . . . 9
|
152 | | volicore 40795 |
. . . . . . . . 9
|
153 | 145, 151,
152 | syl2anc 693 |
. . . . . . . 8
|
154 | 139, 153 | fprodrecl 14683 |
. . . . . . 7
|
155 | 129, 138,
58, 154 | fvmptd 6288 |
. . . . . 6
|
156 | 155 | eqcomd 2628 |
. . . . 5
|
157 | 156 | mpteq2dva 4744 |
. . . 4
|
158 | 157 | fveq2d 6195 |
. . 3
Σ^ Σ^ |
159 | 51 | simprd 479 |
. . 3
Σ^ voln* |
160 | 158, 159 | eqbrtrd 4675 |
. 2
Σ^
voln* |
161 | 93, 127, 160 | jca31 557 |
1
Σ^
voln* |