This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )