Step | Hyp | Ref
| Expression |
1 | | df-rnghomo 41887 |
. . 3
RngHomo Rng Rng |
2 | 1 | a1i 11 |
. 2
Rng Rng
RngHomo Rng Rng |
3 | | fveq2 6191 |
. . . . . . 7
|
4 | | isrnghm.b |
. . . . . . 7
|
5 | 3, 4 | syl6eqr 2674 |
. . . . . 6
|
6 | 5 | csbeq1d 3540 |
. . . . 5
|
7 | | fveq2 6191 |
. . . . . . . 8
|
8 | | rnghmval.c |
. . . . . . . 8
|
9 | 7, 8 | syl6eqr 2674 |
. . . . . . 7
|
10 | 9 | csbeq1d 3540 |
. . . . . 6
|
11 | 10 | csbeq2dv 3992 |
. . . . 5
|
12 | 6, 11 | sylan9eq 2676 |
. . . 4
|
13 | 12 | adantl 482 |
. . 3
Rng
Rng
|
14 | | fvex 6201 |
. . . . . . . 8
|
15 | 4, 14 | eqeltri 2697 |
. . . . . . 7
|
16 | | fvex 6201 |
. . . . . . . 8
|
17 | 8, 16 | eqeltri 2697 |
. . . . . . 7
|
18 | | oveq12 6659 |
. . . . . . . . 9
|
19 | 18 | ancoms 469 |
. . . . . . . 8
|
20 | | raleq 3138 |
. . . . . . . . . 10
|
21 | 20 | raleqbi1dv 3146 |
. . . . . . . . 9
|
22 | 21 | adantr 481 |
. . . . . . . 8
|
23 | 19, 22 | rabeqbidv 3195 |
. . . . . . 7
|
24 | 15, 17, 23 | csbie2 3563 |
. . . . . 6
|
25 | 24 | a1i 11 |
. . . . 5
|
26 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
27 | | rnghmval.p |
. . . . . . . . . . . . 13
|
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
29 | 28 | oveqdr 6674 |
. . . . . . . . . . 11
|
30 | 29 | fveq2d 6195 |
. . . . . . . . . 10
|
31 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
32 | | rnghmval.a |
. . . . . . . . . . . . 13
|
33 | 31, 32 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
34 | 33 | adantl 482 |
. . . . . . . . . . 11
|
35 | 34 | oveqd 6667 |
. . . . . . . . . 10
|
36 | 30, 35 | eqeq12d 2637 |
. . . . . . . . 9
|
37 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
38 | | isrnghm.t |
. . . . . . . . . . . . 13
|
39 | 37, 38 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
40 | 39 | oveqdr 6674 |
. . . . . . . . . . 11
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . 10
|
42 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
43 | | isrnghm.m |
. . . . . . . . . . . . 13
|
44 | 42, 43 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
45 | 44 | adantl 482 |
. . . . . . . . . . 11
|
46 | 45 | oveqd 6667 |
. . . . . . . . . 10
|
47 | 41, 46 | eqeq12d 2637 |
. . . . . . . . 9
|
48 | 36, 47 | anbi12d 747 |
. . . . . . . 8
|
49 | 48 | ralbidv 2986 |
. . . . . . 7
|
50 | 49 | ralbidv 2986 |
. . . . . 6
|
51 | 50 | rabbidv 3189 |
. . . . 5
|
52 | 25, 51 | eqtrd 2656 |
. . . 4
|
53 | 52 | adantl 482 |
. . 3
Rng
Rng
|
54 | 13, 53 | eqtrd 2656 |
. 2
Rng
Rng
|
55 | | simpl 473 |
. 2
Rng Rng
Rng |
56 | | simpr 477 |
. 2
Rng Rng
Rng |
57 | | ovex 6678 |
. . . 4
|
58 | 57 | rabex 4813 |
. . 3
|
59 | 58 | a1i 11 |
. 2
Rng Rng
|
60 | 2, 54, 55, 56, 59 | ovmpt2d 6788 |
1
Rng Rng
RngHomo
|