| Step | Hyp | Ref | Expression | 
						
							| 1 |  | rng2idl1cntr.r |  |-  ( ph -> R e. Rng ) | 
						
							| 2 |  | rng2idl1cntr.i |  |-  ( ph -> I e. ( 2Ideal ` R ) ) | 
						
							| 3 |  | rng2idl1cntr.j |  |-  J = ( R |`s I ) | 
						
							| 4 |  | rng2idl1cntr.u |  |-  ( ph -> J e. Ring ) | 
						
							| 5 |  | rng2idl1cntr.1 |  |-  .1. = ( 1r ` J ) | 
						
							| 6 |  | rng2idl1cntr.m |  |-  M = ( mulGrp ` R ) | 
						
							| 7 |  | eqid |  |-  ( Base ` R ) = ( Base ` R ) | 
						
							| 8 | 3 7 | ressbasss |  |-  ( Base ` J ) C_ ( Base ` R ) | 
						
							| 9 |  | eqid |  |-  ( Base ` J ) = ( Base ` J ) | 
						
							| 10 | 9 5 | ringidcl |  |-  ( J e. Ring -> .1. e. ( Base ` J ) ) | 
						
							| 11 | 4 10 | syl |  |-  ( ph -> .1. e. ( Base ` J ) ) | 
						
							| 12 | 8 11 | sselid |  |-  ( ph -> .1. e. ( Base ` R ) ) | 
						
							| 13 | 1 | adantr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> R e. Rng ) | 
						
							| 14 | 12 | adantr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> .1. e. ( Base ` R ) ) | 
						
							| 15 |  | simpr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> x e. ( Base ` R ) ) | 
						
							| 16 |  | eqid |  |-  ( .r ` R ) = ( .r ` R ) | 
						
							| 17 | 7 16 | rngass |  |-  ( ( R e. Rng /\ ( .1. e. ( Base ` R ) /\ x e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) ) | 
						
							| 18 | 13 14 15 14 17 | syl13anc |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) ) | 
						
							| 19 |  | eqid |  |-  ( .r ` J ) = ( .r ` J ) | 
						
							| 20 | 4 | adantr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> J e. Ring ) | 
						
							| 21 | 1 2 3 4 7 16 5 | rngqiprngghmlem1 |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) x ) e. ( Base ` J ) ) | 
						
							| 22 | 9 19 5 20 21 | ringridmd |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) ) | 
						
							| 23 | 3 16 | ressmulr |  |-  ( I e. ( 2Ideal ` R ) -> ( .r ` R ) = ( .r ` J ) ) | 
						
							| 24 | 2 23 | syl |  |-  ( ph -> ( .r ` R ) = ( .r ` J ) ) | 
						
							| 25 | 24 | oveqd |  |-  ( ph -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) ) | 
						
							| 26 | 25 | eqeq1d |  |-  ( ph -> ( ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) <-> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) ) ) | 
						
							| 27 | 26 | adantr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) <-> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) ) ) | 
						
							| 28 | 22 27 | mpbird |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) ) | 
						
							| 29 | 2 | 2idllidld |  |-  ( ph -> I e. ( LIdeal ` R ) ) | 
						
							| 30 |  | eqid |  |-  ( LIdeal ` R ) = ( LIdeal ` R ) | 
						
							| 31 | 7 30 | lidlss |  |-  ( I e. ( LIdeal ` R ) -> I C_ ( Base ` R ) ) | 
						
							| 32 | 3 7 | ressbas2 |  |-  ( I C_ ( Base ` R ) -> I = ( Base ` J ) ) | 
						
							| 33 | 32 | eqcomd |  |-  ( I C_ ( Base ` R ) -> ( Base ` J ) = I ) | 
						
							| 34 | 29 31 33 | 3syl |  |-  ( ph -> ( Base ` J ) = I ) | 
						
							| 35 | 34 29 | eqeltrd |  |-  ( ph -> ( Base ` J ) e. ( LIdeal ` R ) ) | 
						
							| 36 | 2 3 9 | 2idlbas |  |-  ( ph -> ( Base ` J ) = I ) | 
						
							| 37 |  | ringrng |  |-  ( J e. Ring -> J e. Rng ) | 
						
							| 38 | 4 37 | syl |  |-  ( ph -> J e. Rng ) | 
						
							| 39 | 3 38 | eqeltrrid |  |-  ( ph -> ( R |`s I ) e. Rng ) | 
						
							| 40 | 1 2 39 | rng2idlsubrng |  |-  ( ph -> I e. ( SubRng ` R ) ) | 
						
							| 41 | 36 40 | eqeltrd |  |-  ( ph -> ( Base ` J ) e. ( SubRng ` R ) ) | 
						
							| 42 |  | subrngsubg |  |-  ( ( Base ` J ) e. ( SubRng ` R ) -> ( Base ` J ) e. ( SubGrp ` R ) ) | 
						
							| 43 |  | eqid |  |-  ( 0g ` R ) = ( 0g ` R ) | 
						
							| 44 | 43 | subg0cl |  |-  ( ( Base ` J ) e. ( SubGrp ` R ) -> ( 0g ` R ) e. ( Base ` J ) ) | 
						
							| 45 | 41 42 44 | 3syl |  |-  ( ph -> ( 0g ` R ) e. ( Base ` J ) ) | 
						
							| 46 | 1 35 45 | 3jca |  |-  ( ph -> ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` R ) /\ ( 0g ` R ) e. ( Base ` J ) ) ) | 
						
							| 47 | 11 | anim1ci |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x e. ( Base ` R ) /\ .1. e. ( Base ` J ) ) ) | 
						
							| 48 | 43 7 16 30 | rnglidlmcl |  |-  ( ( ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` R ) /\ ( 0g ` R ) e. ( Base ` J ) ) /\ ( x e. ( Base ` R ) /\ .1. e. ( Base ` J ) ) ) -> ( x ( .r ` R ) .1. ) e. ( Base ` J ) ) | 
						
							| 49 | 46 47 48 | syl2an2r |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) .1. ) e. ( Base ` J ) ) | 
						
							| 50 | 9 19 5 20 49 | ringlidmd |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) | 
						
							| 51 | 24 | oveqd |  |-  ( ph -> ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) ) | 
						
							| 52 | 51 | eqeq1d |  |-  ( ph -> ( ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) <-> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) ) | 
						
							| 53 | 52 | adantr |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) <-> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) ) | 
						
							| 54 | 50 53 | mpbird |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) | 
						
							| 55 | 18 28 54 | 3eqtr3d |  |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) | 
						
							| 56 | 55 | ralrimiva |  |-  ( ph -> A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) | 
						
							| 57 |  | ssidd |  |-  ( ph -> ( Base ` R ) C_ ( Base ` R ) ) | 
						
							| 58 | 6 7 | mgpbas |  |-  ( Base ` R ) = ( Base ` M ) | 
						
							| 59 | 6 16 | mgpplusg |  |-  ( .r ` R ) = ( +g ` M ) | 
						
							| 60 |  | eqid |  |-  ( Cntz ` M ) = ( Cntz ` M ) | 
						
							| 61 | 58 59 60 | elcntz |  |-  ( ( Base ` R ) C_ ( Base ` R ) -> ( .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) <-> ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) ) ) | 
						
							| 62 | 57 61 | syl |  |-  ( ph -> ( .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) <-> ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) ) ) | 
						
							| 63 | 12 56 62 | mpbir2and |  |-  ( ph -> .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) ) | 
						
							| 64 | 58 60 | cntrval |  |-  ( ( Cntz ` M ) ` ( Base ` R ) ) = ( Cntr ` M ) | 
						
							| 65 | 63 64 | eleqtrdi |  |-  ( ph -> .1. e. ( Cntr ` M ) ) |