Step | Hyp | Ref
| Expression |
1 | | nfcv 2764 |
. . . . . 6
|
2 | | nfcv 2764 |
. . . . . 6
|
3 | | nffvmpt1 6199 |
. . . . . . 7
|
4 | | nfcv 2764 |
. . . . . . 7
|
5 | | nfcv 2764 |
. . . . . . 7
|
6 | 3, 4, 5 | nfov 6676 |
. . . . . 6
|
7 | | nfcv 2764 |
. . . . . . 7
|
8 | | nfcv 2764 |
. . . . . . 7
|
9 | | nffvmpt1 6199 |
. . . . . . 7
|
10 | 7, 8, 9 | nfov 6676 |
. . . . . 6
|
11 | | fveq2 6191 |
. . . . . . 7
|
12 | | fveq2 6191 |
. . . . . . 7
|
13 | 11, 12 | oveqan12d 6669 |
. . . . . 6
|
14 | 1, 2, 6, 10, 13 | cbvmpt2 6734 |
. . . . 5
|
15 | | vex 3203 |
. . . . . . . 8
|
16 | | vex 3203 |
. . . . . . . 8
|
17 | 15, 16 | eqop2 7209 |
. . . . . . 7
|
18 | | fveq2 6191 |
. . . . . . . . 9
|
19 | | fveq2 6191 |
. . . . . . . . 9
|
20 | 18, 19 | oveqan12d 6669 |
. . . . . . . 8
|
21 | 20 | adantl 482 |
. . . . . . 7
|
22 | 17, 21 | sylbi 207 |
. . . . . 6
|
23 | 22 | mpt2mpt 6752 |
. . . . 5
|
24 | 14, 23 | eqtr4i 2647 |
. . . 4
|
25 | | simp2 1062 |
. . . . . . 7
|
26 | | evlslem4.x |
. . . . . . . 8
|
27 | 26 | 3adant3 1081 |
. . . . . . 7
|
28 | | eqid 2622 |
. . . . . . . 8
|
29 | 28 | fvmpt2 6291 |
. . . . . . 7
|
30 | 25, 27, 29 | syl2anc 693 |
. . . . . 6
|
31 | | simp3 1063 |
. . . . . . 7
|
32 | | evlslem4.y |
. . . . . . . 8
|
33 | 32 | 3adant2 1080 |
. . . . . . 7
|
34 | | eqid 2622 |
. . . . . . . 8
|
35 | 34 | fvmpt2 6291 |
. . . . . . 7
|
36 | 31, 33, 35 | syl2anc 693 |
. . . . . 6
|
37 | 30, 36 | oveq12d 6668 |
. . . . 5
|
38 | 37 | mpt2eq3dva 6719 |
. . . 4
|
39 | 24, 38 | syl5reqr 2671 |
. . 3
|
40 | 39 | oveq1d 6665 |
. 2
supp
supp
|
41 | | difxp 5558 |
. . . . . 6
supp
supp supp supp |
42 | 41 | eleq2i 2693 |
. . . . 5
supp supp
supp supp |
43 | | elun 3753 |
. . . . 5
supp
supp supp supp |
44 | 42, 43 | bitri 264 |
. . . 4
supp supp
supp supp |
45 | | xp1st 7198 |
. . . . . . . 8
supp supp |
46 | 26, 28 | fmptd 6385 |
. . . . . . . . 9
|
47 | | ssid 3624 |
. . . . . . . . . 10
supp
supp |
48 | 47 | a1i 11 |
. . . . . . . . 9
supp supp |
49 | | evlslem4.i |
. . . . . . . . 9
|
50 | | evlslem4.z |
. . . . . . . . . . 11
|
51 | | fvex 6201 |
. . . . . . . . . . 11
|
52 | 50, 51 | eqeltri 2697 |
. . . . . . . . . 10
|
53 | 52 | a1i 11 |
. . . . . . . . 9
|
54 | 46, 48, 49, 53 | suppssr 7326 |
. . . . . . . 8
supp
|
55 | 45, 54 | sylan2 491 |
. . . . . . 7
supp |
56 | 55 | oveq1d 6665 |
. . . . . 6
supp |
57 | | evlslem4.r |
. . . . . . . 8
|
58 | 57 | adantr 481 |
. . . . . . 7
supp |
59 | 32, 34 | fmptd 6385 |
. . . . . . . 8
|
60 | | xp2nd 7199 |
. . . . . . . 8
supp |
61 | | ffvelrn 6357 |
. . . . . . . 8
|
62 | 59, 60, 61 | syl2an 494 |
. . . . . . 7
supp |
63 | | evlslem4.b |
. . . . . . . 8
|
64 | | evlslem4.t |
. . . . . . . 8
|
65 | 63, 64, 50 | ringlz 18587 |
. . . . . . 7
|
66 | 58, 62, 65 | syl2anc 693 |
. . . . . 6
supp |
67 | 56, 66 | eqtrd 2656 |
. . . . 5
supp |
68 | | xp2nd 7199 |
. . . . . . . 8
supp supp |
69 | | ssid 3624 |
. . . . . . . . . 10
supp
supp |
70 | 69 | a1i 11 |
. . . . . . . . 9
supp supp |
71 | | evlslem4.j |
. . . . . . . . 9
|
72 | 59, 70, 71, 53 | suppssr 7326 |
. . . . . . . 8
supp
|
73 | 68, 72 | sylan2 491 |
. . . . . . 7
supp
|
74 | 73 | oveq2d 6666 |
. . . . . 6
supp
|
75 | 57 | adantr 481 |
. . . . . . 7
supp
|
76 | | xp1st 7198 |
. . . . . . . 8
supp |
77 | | ffvelrn 6357 |
. . . . . . . 8
|
78 | 46, 76, 77 | syl2an 494 |
. . . . . . 7
supp
|
79 | 63, 64, 50 | ringrz 18588 |
. . . . . . 7
|
80 | 75, 78, 79 | syl2anc 693 |
. . . . . 6
supp
|
81 | 74, 80 | eqtrd 2656 |
. . . . 5
supp
|
82 | 67, 81 | jaodan 826 |
. . . 4
supp supp |
83 | 44, 82 | sylan2b 492 |
. . 3
supp supp
|
84 | | xpexg 6960 |
. . . 4
|
85 | 49, 71, 84 | syl2anc 693 |
. . 3
|
86 | 83, 85 | suppss2 7329 |
. 2
supp supp
supp |
87 | 40, 86 | eqsstrd 3639 |
1
supp supp
supp |