Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eropr.1 | |
|
eropr.2 | |
||
eropr.3 | |
||
eropr.4 | |
||
eropr.5 | |
||
eropr.6 | |
||
eropr.7 | |
||
eropr.8 | |
||
eropr.9 | |
||
eropr.10 | |
||
eropr.11 | |
||
eropr.12 | |
||
eropr.13 | |
||
eropr.14 | |
||
Assertion | erov | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eropr.1 | |
|
2 | eropr.2 | |
|
3 | eropr.3 | |
|
4 | eropr.4 | |
|
5 | eropr.5 | |
|
6 | eropr.6 | |
|
7 | eropr.7 | |
|
8 | eropr.8 | |
|
9 | eropr.9 | |
|
10 | eropr.10 | |
|
11 | eropr.11 | |
|
12 | eropr.12 | |
|
13 | eropr.13 | |
|
14 | eropr.14 | |
|
15 | 1 2 3 4 5 6 7 8 9 10 11 12 | erovlem | |
16 | 15 | 3ad2ant1 | |
17 | simprl | |
|
18 | 17 | eqeq1d | |
19 | simprr | |
|
20 | 19 | eqeq1d | |
21 | 18 20 | anbi12d | |
22 | 21 | anbi1d | |
23 | 22 | 2rexbidv | |
24 | 23 | iotabidv | |
25 | ecelqsg | |
|
26 | 25 1 | eleqtrrdi | |
27 | 13 26 | sylan | |
28 | 27 | 3adant3 | |
29 | ecelqsg | |
|
30 | 29 2 | eleqtrrdi | |
31 | 14 30 | sylan | |
32 | 31 | 3adant2 | |
33 | iotaex | |
|
34 | 33 | a1i | |
35 | 16 24 28 32 34 | ovmpod | |
36 | eqid | |
|
37 | eqid | |
|
38 | 36 37 | pm3.2i | |
39 | eqid | |
|
40 | 38 39 | pm3.2i | |
41 | eceq1 | |
|
42 | 41 | eqeq2d | |
43 | 42 | anbi1d | |
44 | oveq1 | |
|
45 | 44 | eceq1d | |
46 | 45 | eqeq2d | |
47 | 43 46 | anbi12d | |
48 | eceq1 | |
|
49 | 48 | eqeq2d | |
50 | 49 | anbi2d | |
51 | oveq2 | |
|
52 | 51 | eceq1d | |
53 | 52 | eqeq2d | |
54 | 50 53 | anbi12d | |
55 | 47 54 | rspc2ev | |
56 | 40 55 | mp3an3 | |
57 | 56 | 3adant1 | |
58 | ecexg | |
|
59 | 3 58 | syl | |
60 | 59 | 3ad2ant1 | |
61 | simp1 | |
|
62 | 1 2 3 4 5 6 7 8 9 10 11 | eroveu | |
63 | 61 28 32 62 | syl12anc | |
64 | simpr | |
|
65 | 64 | eqeq1d | |
66 | 65 | anbi2d | |
67 | 66 | 2rexbidv | |
68 | 60 63 67 | iota2d | |
69 | 57 68 | mpbid | |
70 | 35 69 | eqtrd | |