Step |
Hyp |
Ref |
Expression |
1 |
|
ringpropd.1 |
|- ( ph -> B = ( Base ` K ) ) |
2 |
|
ringpropd.2 |
|- ( ph -> B = ( Base ` L ) ) |
3 |
|
ringpropd.3 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) |
4 |
|
ringpropd.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 |
|
eqid |
|- ( mulGrp ` K ) = ( mulGrp ` K ) |
7 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
8 |
6 7
|
mgpbas |
|- ( Base ` K ) = ( Base ` ( mulGrp ` K ) ) |
9 |
1 8
|
eqtrdi |
|- ( ph -> B = ( Base ` ( mulGrp ` K ) ) ) |
10 |
|
eqid |
|- ( mulGrp ` L ) = ( mulGrp ` L ) |
11 |
|
eqid |
|- ( Base ` L ) = ( Base ` L ) |
12 |
10 11
|
mgpbas |
|- ( Base ` L ) = ( Base ` ( mulGrp ` L ) ) |
13 |
2 12
|
eqtrdi |
|- ( ph -> B = ( Base ` ( mulGrp ` L ) ) ) |
14 |
|
eqid |
|- ( .r ` K ) = ( .r ` K ) |
15 |
6 14
|
mgpplusg |
|- ( .r ` K ) = ( +g ` ( mulGrp ` K ) ) |
16 |
15
|
oveqi |
|- ( x ( .r ` K ) y ) = ( x ( +g ` ( mulGrp ` K ) ) y ) |
17 |
|
eqid |
|- ( .r ` L ) = ( .r ` L ) |
18 |
10 17
|
mgpplusg |
|- ( .r ` L ) = ( +g ` ( mulGrp ` L ) ) |
19 |
18
|
oveqi |
|- ( x ( .r ` L ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) |
20 |
4 16 19
|
3eqtr3g |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) ) |
21 |
9 13 20
|
cmnpropd |
|- ( ph -> ( ( mulGrp ` K ) e. CMnd <-> ( mulGrp ` L ) e. CMnd ) ) |
22 |
5 21
|
anbi12d |
|- ( ph -> ( ( K e. Ring /\ ( mulGrp ` K ) e. CMnd ) <-> ( L e. Ring /\ ( mulGrp ` L ) e. CMnd ) ) ) |
23 |
6
|
iscrng |
|- ( K e. CRing <-> ( K e. Ring /\ ( mulGrp ` K ) e. CMnd ) ) |
24 |
10
|
iscrng |
|- ( L e. CRing <-> ( L e. Ring /\ ( mulGrp ` L ) e. CMnd ) ) |
25 |
22 23 24
|
3bitr4g |
|- ( ph -> ( K e. CRing <-> L e. CRing ) ) |