Step | Hyp | Ref
| Expression |
1 | | elin 3796 |
. . 3
oGrp oGrp |
2 | 1 | anbi1i 731 |
. 2
oGrp
oGrp
|
3 | | fvexd 6203 |
. . . . 5
|
4 | | simpr 477 |
. . . . . . . . . . 11
|
5 | | simpl 473 |
. . . . . . . . . . . . 13
|
6 | 5 | fveq2d 6195 |
. . . . . . . . . . . 12
|
7 | | isorng.2 |
. . . . . . . . . . . 12
|
8 | 6, 7 | syl6eqr 2674 |
. . . . . . . . . . 11
|
9 | 4, 8 | eqtrd 2656 |
. . . . . . . . . 10
|
10 | 9 | oveqd 6667 |
. . . . . . . . 9
|
11 | 10 | breq2d 4665 |
. . . . . . . 8
|
12 | 11 | imbi2d 330 |
. . . . . . 7
|
13 | 12 | 2ralbidv 2989 |
. . . . . 6
|
14 | 13 | sbcbidv 3490 |
. . . . 5
|
15 | 3, 14 | sbcied 3472 |
. . . 4
|
16 | | fvexd 6203 |
. . . . . 6
|
17 | | simpr 477 |
. . . . . . . . . . 11
|
18 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
19 | | isorng.0 |
. . . . . . . . . . . . 13
|
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
21 | 20 | adantr 481 |
. . . . . . . . . . 11
|
22 | 17, 21 | eqtrd 2656 |
. . . . . . . . . 10
|
23 | | raleq 3138 |
. . . . . . . . . . 11
|
24 | 23 | raleqbi1dv 3146 |
. . . . . . . . . 10
|
25 | 22, 24 | syl 17 |
. . . . . . . . 9
|
26 | 25 | sbcbidv 3490 |
. . . . . . . 8
|
27 | 26 | sbcbidv 3490 |
. . . . . . 7
|
28 | 27 | sbcbidv 3490 |
. . . . . 6
|
29 | 16, 28 | sbcied 3472 |
. . . . 5
|
30 | | fvexd 6203 |
. . . . . 6
|
31 | | simpr 477 |
. . . . . . . . . . . . 13
|
32 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
33 | | isorng.1 |
. . . . . . . . . . . . . . 15
|
34 | 32, 33 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . 13
|
36 | 31, 35 | eqtrd 2656 |
. . . . . . . . . . . 12
|
37 | 36 | breq1d 4663 |
. . . . . . . . . . 11
|
38 | 36 | breq1d 4663 |
. . . . . . . . . . 11
|
39 | 37, 38 | anbi12d 747 |
. . . . . . . . . 10
|
40 | 36 | breq1d 4663 |
. . . . . . . . . 10
|
41 | 39, 40 | imbi12d 334 |
. . . . . . . . 9
|
42 | 41 | 2ralbidv 2989 |
. . . . . . . 8
|
43 | 42 | sbcbidv 3490 |
. . . . . . 7
|
44 | 43 | sbcbidv 3490 |
. . . . . 6
|
45 | 30, 44 | sbcied 3472 |
. . . . 5
|
46 | 29, 45 | bitr2d 269 |
. . . 4
|
47 | | fvexd 6203 |
. . . . 5
|
48 | | simpr 477 |
. . . . . . . . . 10
|
49 | | simpl 473 |
. . . . . . . . . . . 12
|
50 | 49 | fveq2d 6195 |
. . . . . . . . . . 11
|
51 | | isorng.3 |
. . . . . . . . . . 11
|
52 | 50, 51 | syl6eqr 2674 |
. . . . . . . . . 10
|
53 | 48, 52 | eqtrd 2656 |
. . . . . . . . 9
|
54 | 53 | breqd 4664 |
. . . . . . . 8
|
55 | 53 | breqd 4664 |
. . . . . . . 8
|
56 | 54, 55 | anbi12d 747 |
. . . . . . 7
|
57 | 53 | breqd 4664 |
. . . . . . 7
|
58 | 56, 57 | imbi12d 334 |
. . . . . 6
|
59 | 58 | 2ralbidv 2989 |
. . . . 5
|
60 | 47, 59 | sbcied 3472 |
. . . 4
|
61 | 15, 46, 60 | 3bitr3d 298 |
. . 3
|
62 | | df-orng 29797 |
. . 3
oRing oGrp
|
63 | 61, 62 | elrab2 3366 |
. 2
oRing oGrp
|
64 | | df-3an 1039 |
. 2
oGrp
oGrp
|
65 | 2, 63, 64 | 3bitr4i 292 |
1
oRing oGrp
|