| Step | Hyp | Ref | Expression | 
						
							| 1 |  | rngqiprngfu.r |  |-  ( ph -> R e. Rng ) | 
						
							| 2 |  | rngqiprngfu.i |  |-  ( ph -> I e. ( 2Ideal ` R ) ) | 
						
							| 3 |  | rngqiprngfu.j |  |-  J = ( R |`s I ) | 
						
							| 4 |  | rngqiprngfu.u |  |-  ( ph -> J e. Ring ) | 
						
							| 5 |  | rngqiprngfu.b |  |-  B = ( Base ` R ) | 
						
							| 6 |  | rngqiprngfu.t |  |-  .x. = ( .r ` R ) | 
						
							| 7 |  | rngqiprngfu.1 |  |-  .1. = ( 1r ` J ) | 
						
							| 8 |  | rngqiprngfu.g |  |-  .~ = ( R ~QG I ) | 
						
							| 9 |  | rngqiprngfu.q |  |-  Q = ( R /s .~ ) | 
						
							| 10 |  | rngqiprngfu.v |  |-  ( ph -> Q e. Ring ) | 
						
							| 11 |  | rngqiprngfu.e |  |-  ( ph -> E e. ( 1r ` Q ) ) | 
						
							| 12 |  | rngqiprngfu.m |  |-  .- = ( -g ` R ) | 
						
							| 13 |  | rngqiprngfu.a |  |-  .+ = ( +g ` R ) | 
						
							| 14 |  | rngqiprngfu.n |  |-  U = ( ( E .- ( .1. .x. E ) ) .+ .1. ) | 
						
							| 15 | 14 | oveq2i |  |-  ( E .- U ) = ( E .- ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) | 
						
							| 16 | 15 | a1i |  |-  ( ph -> ( E .- U ) = ( E .- ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) ) | 
						
							| 17 |  | rngabl |  |-  ( R e. Rng -> R e. Abel ) | 
						
							| 18 | 1 17 | syl |  |-  ( ph -> R e. Abel ) | 
						
							| 19 | 1 2 3 4 5 6 7 8 9 10 11 | rngqiprngfulem2 |  |-  ( ph -> E e. B ) | 
						
							| 20 |  | rnggrp |  |-  ( R e. Rng -> R e. Grp ) | 
						
							| 21 | 1 20 | syl |  |-  ( ph -> R e. Grp ) | 
						
							| 22 | 1 2 3 4 5 6 7 | rngqiprng1elbas |  |-  ( ph -> .1. e. B ) | 
						
							| 23 | 5 6 | rngcl |  |-  ( ( R e. Rng /\ .1. e. B /\ E e. B ) -> ( .1. .x. E ) e. B ) | 
						
							| 24 | 1 22 19 23 | syl3anc |  |-  ( ph -> ( .1. .x. E ) e. B ) | 
						
							| 25 | 5 12 | grpsubcl |  |-  ( ( R e. Grp /\ E e. B /\ ( .1. .x. E ) e. B ) -> ( E .- ( .1. .x. E ) ) e. B ) | 
						
							| 26 | 21 19 24 25 | syl3anc |  |-  ( ph -> ( E .- ( .1. .x. E ) ) e. B ) | 
						
							| 27 | 5 13 12 18 19 26 22 | ablsubsub4 |  |-  ( ph -> ( ( E .- ( E .- ( .1. .x. E ) ) ) .- .1. ) = ( E .- ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) ) | 
						
							| 28 | 5 12 18 19 24 | ablnncan |  |-  ( ph -> ( E .- ( E .- ( .1. .x. E ) ) ) = ( .1. .x. E ) ) | 
						
							| 29 | 28 | oveq1d |  |-  ( ph -> ( ( E .- ( E .- ( .1. .x. E ) ) ) .- .1. ) = ( ( .1. .x. E ) .- .1. ) ) | 
						
							| 30 | 16 27 29 | 3eqtr2d |  |-  ( ph -> ( E .- U ) = ( ( .1. .x. E ) .- .1. ) ) | 
						
							| 31 |  | ringrng |  |-  ( J e. Ring -> J e. Rng ) | 
						
							| 32 | 4 31 | syl |  |-  ( ph -> J e. Rng ) | 
						
							| 33 | 3 32 | eqeltrrid |  |-  ( ph -> ( R |`s I ) e. Rng ) | 
						
							| 34 | 1 2 33 | rng2idlnsg |  |-  ( ph -> I e. ( NrmSGrp ` R ) ) | 
						
							| 35 |  | nsgsubg |  |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) ) | 
						
							| 36 | 34 35 | syl |  |-  ( ph -> I e. ( SubGrp ` R ) ) | 
						
							| 37 | 1 2 3 4 5 6 7 | rngqiprngghmlem1 |  |-  ( ( ph /\ E e. B ) -> ( .1. .x. E ) e. ( Base ` J ) ) | 
						
							| 38 | 19 37 | mpdan |  |-  ( ph -> ( .1. .x. E ) e. ( Base ` J ) ) | 
						
							| 39 |  | eqid |  |-  ( Base ` J ) = ( Base ` J ) | 
						
							| 40 | 2 3 39 | 2idlbas |  |-  ( ph -> ( Base ` J ) = I ) | 
						
							| 41 | 38 40 | eleqtrd |  |-  ( ph -> ( .1. .x. E ) e. I ) | 
						
							| 42 | 39 7 | ringidcl |  |-  ( J e. Ring -> .1. e. ( Base ` J ) ) | 
						
							| 43 | 4 42 | syl |  |-  ( ph -> .1. e. ( Base ` J ) ) | 
						
							| 44 | 43 40 | eleqtrd |  |-  ( ph -> .1. e. I ) | 
						
							| 45 |  | eqid |  |-  ( -g ` J ) = ( -g ` J ) | 
						
							| 46 | 12 3 45 | subgsub |  |-  ( ( I e. ( SubGrp ` R ) /\ ( .1. .x. E ) e. I /\ .1. e. I ) -> ( ( .1. .x. E ) .- .1. ) = ( ( .1. .x. E ) ( -g ` J ) .1. ) ) | 
						
							| 47 | 36 41 44 46 | syl3anc |  |-  ( ph -> ( ( .1. .x. E ) .- .1. ) = ( ( .1. .x. E ) ( -g ` J ) .1. ) ) | 
						
							| 48 | 4 | ringgrpd |  |-  ( ph -> J e. Grp ) | 
						
							| 49 | 39 45 | grpsubcl |  |-  ( ( J e. Grp /\ ( .1. .x. E ) e. ( Base ` J ) /\ .1. e. ( Base ` J ) ) -> ( ( .1. .x. E ) ( -g ` J ) .1. ) e. ( Base ` J ) ) | 
						
							| 50 | 48 38 43 49 | syl3anc |  |-  ( ph -> ( ( .1. .x. E ) ( -g ` J ) .1. ) e. ( Base ` J ) ) | 
						
							| 51 | 47 50 | eqeltrd |  |-  ( ph -> ( ( .1. .x. E ) .- .1. ) e. ( Base ` J ) ) | 
						
							| 52 | 51 40 | eleqtrd |  |-  ( ph -> ( ( .1. .x. E ) .- .1. ) e. I ) | 
						
							| 53 | 30 52 | eqeltrd |  |-  ( ph -> ( E .- U ) e. I ) | 
						
							| 54 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | rngqiprngfulem3 |  |-  ( ph -> U e. B ) | 
						
							| 55 | 5 12 8 | qusecsub |  |-  ( ( ( R e. Abel /\ I e. ( SubGrp ` R ) ) /\ ( U e. B /\ E e. B ) ) -> ( [ U ] .~ = [ E ] .~ <-> ( E .- U ) e. I ) ) | 
						
							| 56 | 18 36 54 19 55 | syl22anc |  |-  ( ph -> ( [ U ] .~ = [ E ] .~ <-> ( E .- U ) e. I ) ) | 
						
							| 57 | 53 56 | mpbird |  |-  ( ph -> [ U ] .~ = [ E ] .~ ) |