Step |
Hyp |
Ref |
Expression |
1 |
|
isdivrng1.1 |
|- G = ( 1st ` R ) |
2 |
|
isdivrng1.2 |
|- H = ( 2nd ` R ) |
3 |
|
isdivrng1.3 |
|- Z = ( GId ` G ) |
4 |
|
isdivrng1.4 |
|- X = ran G |
5 |
|
df-drngo |
|- DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) } |
6 |
5
|
relopabi |
|- Rel DivRingOps |
7 |
|
1st2nd |
|- ( ( Rel DivRingOps /\ R e. DivRingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
8 |
6 7
|
mpan |
|- ( R e. DivRingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
9 |
|
relrngo |
|- Rel RingOps |
10 |
|
1st2nd |
|- ( ( Rel RingOps /\ R e. RingOps ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
11 |
9 10
|
mpan |
|- ( R e. RingOps -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
12 |
11
|
adantr |
|- ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
13 |
1 2
|
opeq12i |
|- <. G , H >. = <. ( 1st ` R ) , ( 2nd ` R ) >. |
14 |
13
|
eqeq2i |
|- ( R = <. G , H >. <-> R = <. ( 1st ` R ) , ( 2nd ` R ) >. ) |
15 |
2
|
fvexi |
|- H e. _V |
16 |
|
isdivrngo |
|- ( H e. _V -> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) ) |
17 |
15 16
|
ax-mp |
|- ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) |
18 |
3
|
sneqi |
|- { Z } = { ( GId ` G ) } |
19 |
4 18
|
difeq12i |
|- ( X \ { Z } ) = ( ran G \ { ( GId ` G ) } ) |
20 |
19 19
|
xpeq12i |
|- ( ( X \ { Z } ) X. ( X \ { Z } ) ) = ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) |
21 |
20
|
reseq2i |
|- ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) |
22 |
21
|
eleq1i |
|- ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp <-> ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) |
23 |
22
|
anbi2i |
|- ( ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( ran G \ { ( GId ` G ) } ) X. ( ran G \ { ( GId ` G ) } ) ) ) e. GrpOp ) ) |
24 |
17 23
|
bitr4i |
|- ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) |
25 |
|
eleq1 |
|- ( R = <. G , H >. -> ( R e. DivRingOps <-> <. G , H >. e. DivRingOps ) ) |
26 |
|
eleq1 |
|- ( R = <. G , H >. -> ( R e. RingOps <-> <. G , H >. e. RingOps ) ) |
27 |
26
|
anbi1d |
|- ( R = <. G , H >. -> ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) ) |
28 |
25 27
|
bibi12d |
|- ( R = <. G , H >. -> ( ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) <-> ( <. G , H >. e. DivRingOps <-> ( <. G , H >. e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) ) ) |
29 |
24 28
|
mpbiri |
|- ( R = <. G , H >. -> ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) ) |
30 |
14 29
|
sylbir |
|- ( R = <. ( 1st ` R ) , ( 2nd ` R ) >. -> ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) ) |
31 |
8 12 30
|
pm5.21nii |
|- ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) ) |