Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. 2
mzPoly
mzPoly |
2 | | elfvex 6221 |
. . 3
mzPoly
|
3 | 2 | 3ad2ant2 1083 |
. 2
mzPoly
mzPoly |
4 | | simp3 1063 |
. 2
mzPoly
mzPoly
mzPoly |
5 | | simp2 1062 |
. 2
mzPoly
mzPoly mzPoly |
6 | | simpr 477 |
. . . . . . 7
mzPoly
|
7 | | simpll3 1102 |
. . . . . . 7
mzPoly
mzPoly |
8 | | simpll2 1101 |
. . . . . . 7
mzPoly
|
9 | | mzpf 37299 |
. . . . . . . . . . . . . 14
mzPoly
|
10 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
mzPoly |
11 | 10 | expcom 451 |
. . . . . . . . . . . 12
mzPoly
|
12 | 11 | ralimdv 2963 |
. . . . . . . . . . 11
mzPoly
|
13 | 12 | imp 445 |
. . . . . . . . . 10
mzPoly
|
14 | | eqid 2622 |
. . . . . . . . . . 11
|
15 | 14 | fmpt 6381 |
. . . . . . . . . 10
|
16 | 13, 15 | sylib 208 |
. . . . . . . . 9
mzPoly
|
17 | 16 | adantr 481 |
. . . . . . . 8
mzPoly
|
18 | | zex 11386 |
. . . . . . . . 9
|
19 | | simpr 477 |
. . . . . . . . 9
mzPoly
|
20 | | elmapg 7870 |
. . . . . . . . 9
|
21 | 18, 19, 20 | sylancr 695 |
. . . . . . . 8
mzPoly
|
22 | 17, 21 | mpbird 247 |
. . . . . . 7
mzPoly
|
23 | 6, 7, 8, 22 | syl21anc 1325 |
. . . . . 6
mzPoly
|
24 | | vex 3203 |
. . . . . . 7
|
25 | 24 | fvconst2 6469 |
. . . . . 6
|
26 | 23, 25 | syl 17 |
. . . . 5
mzPoly
|
27 | 26 | mpteq2dva 4744 |
. . . 4
mzPoly
|
28 | | mzpconstmpt 37303 |
. . . . 5
mzPoly |
29 | 28 | 3ad2antl1 1223 |
. . . 4
mzPoly
mzPoly |
30 | 27, 29 | eqeltrd 2701 |
. . 3
mzPoly
mzPoly |
31 | | simpr 477 |
. . . . . . . . 9
mzPoly
|
32 | | simpll3 1102 |
. . . . . . . . 9
mzPoly
mzPoly |
33 | | simpll2 1101 |
. . . . . . . . 9
mzPoly
|
34 | 31, 32, 33, 22 | syl21anc 1325 |
. . . . . . . 8
mzPoly
|
35 | | fveq1 6190 |
. . . . . . . . 9
|
36 | | eqid 2622 |
. . . . . . . . 9
|
37 | | fvex 6201 |
. . . . . . . . 9
|
38 | 35, 36, 37 | fvmpt 6282 |
. . . . . . . 8
|
39 | 34, 38 | syl 17 |
. . . . . . 7
mzPoly
|
40 | | simplr 792 |
. . . . . . . 8
mzPoly
|
41 | | fvex 6201 |
. . . . . . . 8
|
42 | | csbeq1 3536 |
. . . . . . . . . 10
|
43 | 42 | fveq1d 6193 |
. . . . . . . . 9
|
44 | | nfcv 2764 |
. . . . . . . . . 10
|
45 | | nfcsb1v 3549 |
. . . . . . . . . . 11
|
46 | | nfcv 2764 |
. . . . . . . . . . 11
|
47 | 45, 46 | nffv 6198 |
. . . . . . . . . 10
|
48 | | csbeq1a 3542 |
. . . . . . . . . . 11
|
49 | 48 | fveq1d 6193 |
. . . . . . . . . 10
|
50 | 44, 47, 49 | cbvmpt 4749 |
. . . . . . . . 9
|
51 | 43, 50 | fvmptg 6280 |
. . . . . . . 8
|
52 | 40, 41, 51 | sylancl 694 |
. . . . . . 7
mzPoly
|
53 | 39, 52 | eqtrd 2656 |
. . . . . 6
mzPoly
|
54 | 53 | mpteq2dva 4744 |
. . . . 5
mzPoly
|
55 | | simpr 477 |
. . . . . . . 8
mzPoly
|
56 | | simpl3 1066 |
. . . . . . . 8
mzPoly
mzPoly |
57 | | nfcsb1v 3549 |
. . . . . . . . . 10
|
58 | 57 | nfel1 2779 |
. . . . . . . . 9
mzPoly |
59 | | csbeq1a 3542 |
. . . . . . . . . 10
|
60 | 59 | eleq1d 2686 |
. . . . . . . . 9
mzPoly
mzPoly |
61 | 58, 60 | rspc 3303 |
. . . . . . . 8
mzPoly
mzPoly |
62 | 55, 56, 61 | sylc 65 |
. . . . . . 7
mzPoly
mzPoly |
63 | | mzpf 37299 |
. . . . . . 7
mzPoly |
64 | 62, 63 | syl 17 |
. . . . . 6
mzPoly
|
65 | 64 | feqmptd 6249 |
. . . . 5
mzPoly
|
66 | 54, 65 | eqtr4d 2659 |
. . . 4
mzPoly
|
67 | 66, 62 | eqeltrd 2701 |
. . 3
mzPoly
mzPoly |
68 | | simp2l 1087 |
. . . . . 6
mzPoly
mzPoly mzPoly |
69 | | ffn 6045 |
. . . . . 6
|
70 | 68, 69 | syl 17 |
. . . . 5
mzPoly
mzPoly mzPoly |
71 | | simp3l 1089 |
. . . . . 6
mzPoly
mzPoly mzPoly |
72 | | ffn 6045 |
. . . . . 6
|
73 | 71, 72 | syl 17 |
. . . . 5
mzPoly
mzPoly mzPoly |
74 | | simp13 1093 |
. . . . 5
mzPoly
mzPoly mzPoly
mzPoly |
75 | | simp12 1092 |
. . . . 5
mzPoly
mzPoly mzPoly |
76 | | simplll 798 |
. . . . . . 7
mzPoly
|
77 | | simpllr 799 |
. . . . . . 7
mzPoly
|
78 | | ovexd 6680 |
. . . . . . 7
mzPoly
|
79 | | simpr 477 |
. . . . . . . . . 10
mzPoly
|
80 | | simplrl 800 |
. . . . . . . . . 10
mzPoly
mzPoly |
81 | 79, 80, 12 | sylc 65 |
. . . . . . . . 9
mzPoly
|
82 | 81, 15 | sylib 208 |
. . . . . . . 8
mzPoly
|
83 | | simplrr 801 |
. . . . . . . . 9
mzPoly
|
84 | 18, 83, 20 | sylancr 695 |
. . . . . . . 8
mzPoly
|
85 | 82, 84 | mpbird 247 |
. . . . . . 7
mzPoly
|
86 | | fnfvof 6911 |
. . . . . . 7
|
87 | 76, 77, 78, 85, 86 | syl22anc 1327 |
. . . . . 6
mzPoly
|
88 | 87 | mpteq2dva 4744 |
. . . . 5
mzPoly
|
89 | 70, 73, 74, 75, 88 | syl22anc 1327 |
. . . 4
mzPoly
mzPoly mzPoly |
90 | | simp2r 1088 |
. . . . 5
mzPoly
mzPoly mzPoly mzPoly |
91 | | simp3r 1090 |
. . . . 5
mzPoly
mzPoly mzPoly mzPoly |
92 | | mzpaddmpt 37304 |
. . . . 5
mzPoly mzPoly
mzPoly |
93 | 90, 91, 92 | syl2anc 693 |
. . . 4
mzPoly
mzPoly mzPoly mzPoly |
94 | 89, 93 | eqeltrd 2701 |
. . 3
mzPoly
mzPoly mzPoly mzPoly |
95 | | fnfvof 6911 |
. . . . . . 7
|
96 | 76, 77, 78, 85, 95 | syl22anc 1327 |
. . . . . 6
mzPoly
|
97 | 96 | mpteq2dva 4744 |
. . . . 5
mzPoly
|
98 | 70, 73, 74, 75, 97 | syl22anc 1327 |
. . . 4
mzPoly
mzPoly mzPoly
|
99 | | mzpmulmpt 37305 |
. . . . 5
mzPoly mzPoly
mzPoly |
100 | 90, 91, 99 | syl2anc 693 |
. . . 4
mzPoly
mzPoly mzPoly mzPoly |
101 | 98, 100 | eqeltrd 2701 |
. . 3
mzPoly
mzPoly mzPoly
mzPoly |
102 | | fveq1 6190 |
. . . . 5
|
103 | 102 | mpteq2dv 4745 |
. . . 4
|
104 | 103 | eleq1d 2686 |
. . 3
mzPoly
mzPoly |
105 | | fveq1 6190 |
. . . . 5
|
106 | 105 | mpteq2dv 4745 |
. . . 4
|
107 | 106 | eleq1d 2686 |
. . 3
mzPoly mzPoly |
108 | | fveq1 6190 |
. . . . 5
|
109 | 108 | mpteq2dv 4745 |
. . . 4
|
110 | 109 | eleq1d 2686 |
. . 3
mzPoly mzPoly |
111 | | fveq1 6190 |
. . . . 5
|
112 | 111 | mpteq2dv 4745 |
. . . 4
|
113 | 112 | eleq1d 2686 |
. . 3
mzPoly mzPoly |
114 | | fveq1 6190 |
. . . . 5
|
115 | 114 | mpteq2dv 4745 |
. . . 4
|
116 | 115 | eleq1d 2686 |
. . 3
mzPoly
mzPoly |
117 | | fveq1 6190 |
. . . . 5
|
118 | 117 | mpteq2dv 4745 |
. . . 4
|
119 | 118 | eleq1d 2686 |
. . 3
mzPoly
mzPoly |
120 | | fveq1 6190 |
. . . . 5
|
121 | 120 | mpteq2dv 4745 |
. . . 4
|
122 | 121 | eleq1d 2686 |
. . 3
mzPoly mzPoly |
123 | 30, 67, 94, 101, 104, 107, 110, 113, 116, 119, 122 | mzpindd 37309 |
. 2
mzPoly
mzPoly mzPoly |
124 | 1, 3, 4, 5, 123 | syl31anc 1329 |
1
mzPoly
mzPoly mzPoly |