Step |
Hyp |
Ref |
Expression |
1 |
|
idllmulcl.1 |
|- G = ( 1st ` R ) |
2 |
|
idllmulcl.2 |
|- H = ( 2nd ` R ) |
3 |
|
idllmulcl.3 |
|- X = ran G |
4 |
|
eqid |
|- ( GId ` G ) = ( GId ` G ) |
5 |
1 2 3 4
|
isidl |
|- ( R e. RingOps -> ( I e. ( Idl ` R ) <-> ( I C_ X /\ ( GId ` G ) e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) ) ) |
6 |
5
|
biimpa |
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( I C_ X /\ ( GId ` G ) e. I /\ A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) ) |
7 |
6
|
simp3d |
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) ) |
8 |
|
simpl |
|- ( ( ( z H x ) e. I /\ ( x H z ) e. I ) -> ( z H x ) e. I ) |
9 |
8
|
ralimi |
|- ( A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) -> A. z e. X ( z H x ) e. I ) |
10 |
9
|
adantl |
|- ( ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) -> A. z e. X ( z H x ) e. I ) |
11 |
10
|
ralimi |
|- ( A. x e. I ( A. y e. I ( x G y ) e. I /\ A. z e. X ( ( z H x ) e. I /\ ( x H z ) e. I ) ) -> A. x e. I A. z e. X ( z H x ) e. I ) |
12 |
7 11
|
syl |
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> A. x e. I A. z e. X ( z H x ) e. I ) |
13 |
|
oveq2 |
|- ( x = A -> ( z H x ) = ( z H A ) ) |
14 |
13
|
eleq1d |
|- ( x = A -> ( ( z H x ) e. I <-> ( z H A ) e. I ) ) |
15 |
|
oveq1 |
|- ( z = B -> ( z H A ) = ( B H A ) ) |
16 |
15
|
eleq1d |
|- ( z = B -> ( ( z H A ) e. I <-> ( B H A ) e. I ) ) |
17 |
14 16
|
rspc2v |
|- ( ( A e. I /\ B e. X ) -> ( A. x e. I A. z e. X ( z H x ) e. I -> ( B H A ) e. I ) ) |
18 |
12 17
|
mpan9 |
|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. X ) ) -> ( B H A ) e. I ) |