Metamath Proof Explorer


Theorem idllmulcl

Description: An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idllmulcl.1
|- G = ( 1st ` R )
idllmulcl.2
|- H = ( 2nd ` R )
idllmulcl.3
|- X = ran G
Assertion idllmulcl
|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( A e. I /\ B e. X ) ) -> ( B H A ) e. I )

Proof

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 )