Step |
Hyp |
Ref |
Expression |
1 |
|
subrgpropd.1 |
|- ( ph -> B = ( Base ` K ) ) |
2 |
|
subrgpropd.2 |
|- ( ph -> B = ( Base ` L ) ) |
3 |
|
subrgpropd.3 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) |
4 |
|
subrgpropd.4 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) |
5 |
1 2 3 4
|
ringpropd |
|- ( ph -> ( K e. Ring <-> L e. Ring ) ) |
6 |
1
|
ineq2d |
|- ( ph -> ( s i^i B ) = ( s i^i ( Base ` K ) ) ) |
7 |
|
eqid |
|- ( K |`s s ) = ( K |`s s ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
7 8
|
ressbas |
|- ( s e. _V -> ( s i^i ( Base ` K ) ) = ( Base ` ( K |`s s ) ) ) |
10 |
9
|
elv |
|- ( s i^i ( Base ` K ) ) = ( Base ` ( K |`s s ) ) |
11 |
6 10
|
eqtrdi |
|- ( ph -> ( s i^i B ) = ( Base ` ( K |`s s ) ) ) |
12 |
2
|
ineq2d |
|- ( ph -> ( s i^i B ) = ( s i^i ( Base ` L ) ) ) |
13 |
|
eqid |
|- ( L |`s s ) = ( L |`s s ) |
14 |
|
eqid |
|- ( Base ` L ) = ( Base ` L ) |
15 |
13 14
|
ressbas |
|- ( s e. _V -> ( s i^i ( Base ` L ) ) = ( Base ` ( L |`s s ) ) ) |
16 |
15
|
elv |
|- ( s i^i ( Base ` L ) ) = ( Base ` ( L |`s s ) ) |
17 |
12 16
|
eqtrdi |
|- ( ph -> ( s i^i B ) = ( Base ` ( L |`s s ) ) ) |
18 |
|
elinel2 |
|- ( x e. ( s i^i B ) -> x e. B ) |
19 |
|
elinel2 |
|- ( y e. ( s i^i B ) -> y e. B ) |
20 |
18 19
|
anim12i |
|- ( ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) -> ( x e. B /\ y e. B ) ) |
21 |
|
eqid |
|- ( +g ` K ) = ( +g ` K ) |
22 |
7 21
|
ressplusg |
|- ( s e. _V -> ( +g ` K ) = ( +g ` ( K |`s s ) ) ) |
23 |
22
|
elv |
|- ( +g ` K ) = ( +g ` ( K |`s s ) ) |
24 |
23
|
oveqi |
|- ( x ( +g ` K ) y ) = ( x ( +g ` ( K |`s s ) ) y ) |
25 |
|
eqid |
|- ( +g ` L ) = ( +g ` L ) |
26 |
13 25
|
ressplusg |
|- ( s e. _V -> ( +g ` L ) = ( +g ` ( L |`s s ) ) ) |
27 |
26
|
elv |
|- ( +g ` L ) = ( +g ` ( L |`s s ) ) |
28 |
27
|
oveqi |
|- ( x ( +g ` L ) y ) = ( x ( +g ` ( L |`s s ) ) y ) |
29 |
3 24 28
|
3eqtr3g |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( K |`s s ) ) y ) = ( x ( +g ` ( L |`s s ) ) y ) ) |
30 |
20 29
|
sylan2 |
|- ( ( ph /\ ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) ) -> ( x ( +g ` ( K |`s s ) ) y ) = ( x ( +g ` ( L |`s s ) ) y ) ) |
31 |
|
eqid |
|- ( .r ` K ) = ( .r ` K ) |
32 |
7 31
|
ressmulr |
|- ( s e. _V -> ( .r ` K ) = ( .r ` ( K |`s s ) ) ) |
33 |
32
|
elv |
|- ( .r ` K ) = ( .r ` ( K |`s s ) ) |
34 |
33
|
oveqi |
|- ( x ( .r ` K ) y ) = ( x ( .r ` ( K |`s s ) ) y ) |
35 |
|
eqid |
|- ( .r ` L ) = ( .r ` L ) |
36 |
13 35
|
ressmulr |
|- ( s e. _V -> ( .r ` L ) = ( .r ` ( L |`s s ) ) ) |
37 |
36
|
elv |
|- ( .r ` L ) = ( .r ` ( L |`s s ) ) |
38 |
37
|
oveqi |
|- ( x ( .r ` L ) y ) = ( x ( .r ` ( L |`s s ) ) y ) |
39 |
4 34 38
|
3eqtr3g |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` ( K |`s s ) ) y ) = ( x ( .r ` ( L |`s s ) ) y ) ) |
40 |
20 39
|
sylan2 |
|- ( ( ph /\ ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) ) -> ( x ( .r ` ( K |`s s ) ) y ) = ( x ( .r ` ( L |`s s ) ) y ) ) |
41 |
11 17 30 40
|
ringpropd |
|- ( ph -> ( ( K |`s s ) e. Ring <-> ( L |`s s ) e. Ring ) ) |
42 |
5 41
|
anbi12d |
|- ( ph -> ( ( K e. Ring /\ ( K |`s s ) e. Ring ) <-> ( L e. Ring /\ ( L |`s s ) e. Ring ) ) ) |
43 |
1 2
|
eqtr3d |
|- ( ph -> ( Base ` K ) = ( Base ` L ) ) |
44 |
43
|
sseq2d |
|- ( ph -> ( s C_ ( Base ` K ) <-> s C_ ( Base ` L ) ) ) |
45 |
1 2 4
|
rngidpropd |
|- ( ph -> ( 1r ` K ) = ( 1r ` L ) ) |
46 |
45
|
eleq1d |
|- ( ph -> ( ( 1r ` K ) e. s <-> ( 1r ` L ) e. s ) ) |
47 |
44 46
|
anbi12d |
|- ( ph -> ( ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) <-> ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) ) |
48 |
42 47
|
anbi12d |
|- ( ph -> ( ( ( K e. Ring /\ ( K |`s s ) e. Ring ) /\ ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) ) <-> ( ( L e. Ring /\ ( L |`s s ) e. Ring ) /\ ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) ) ) |
49 |
|
eqid |
|- ( 1r ` K ) = ( 1r ` K ) |
50 |
8 49
|
issubrg |
|- ( s e. ( SubRing ` K ) <-> ( ( K e. Ring /\ ( K |`s s ) e. Ring ) /\ ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) ) ) |
51 |
|
eqid |
|- ( 1r ` L ) = ( 1r ` L ) |
52 |
14 51
|
issubrg |
|- ( s e. ( SubRing ` L ) <-> ( ( L e. Ring /\ ( L |`s s ) e. Ring ) /\ ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) ) |
53 |
48 50 52
|
3bitr4g |
|- ( ph -> ( s e. ( SubRing ` K ) <-> s e. ( SubRing ` L ) ) ) |
54 |
53
|
eqrdv |
|- ( ph -> ( SubRing ` K ) = ( SubRing ` L ) ) |