Step |
Hyp |
Ref |
Expression |
1 |
|
drngpropd.1 |
|- ( ph -> B = ( Base ` K ) ) |
2 |
|
drngpropd.2 |
|- ( ph -> B = ( Base ` L ) ) |
3 |
|
drngpropd.3 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) |
4 |
|
drngpropd.4 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) |
5 |
1 2 3 4
|
drngpropd |
|- ( ph -> ( K e. DivRing <-> L e. DivRing ) ) |
6 |
1 2 3 4
|
crngpropd |
|- ( ph -> ( K e. CRing <-> L e. CRing ) ) |
7 |
5 6
|
anbi12d |
|- ( ph -> ( ( K e. DivRing /\ K e. CRing ) <-> ( L e. DivRing /\ L e. CRing ) ) ) |
8 |
|
isfld |
|- ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) ) |
9 |
|
isfld |
|- ( L e. Field <-> ( L e. DivRing /\ L e. CRing ) ) |
10 |
7 8 9
|
3bitr4g |
|- ( ph -> ( K e. Field <-> L e. Field ) ) |