Metamath Proof Explorer

Theorem rngqiprngfulem4

Description: Lemma 4 for rngqiprngfu . (Contributed by AV, 16-Mar-2025)

Ref Expression
Hypotheses rngqiprngfu.r 
|- ( ph -> R e. Rng )
rngqiprngfu.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rngqiprngfu.j 
|- J = ( R |`s I )
rngqiprngfu.u 
|- ( ph -> J e. Ring )
rngqiprngfu.b 
|- B = ( Base ` R )
rngqiprngfu.t 
|- .x. = ( .r ` R )
rngqiprngfu.1 
|- .1. = ( 1r ` J )
rngqiprngfu.g 
|- .~ = ( R ~QG I )
rngqiprngfu.q 
|- Q = ( R /s .~ )
rngqiprngfu.v 
|- ( ph -> Q e. Ring )
rngqiprngfu.e 
|- ( ph -> E e. ( 1r ` Q ) )
rngqiprngfu.m 
|- .- = ( -g ` R )
rngqiprngfu.a 
|- .+ = ( +g ` R )
rngqiprngfu.n 
|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
Assertion rngqiprngfulem4 
|- ( ph -> [ U ] .~ = [ E ] .~ )

Proof

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 ] .~ )