Metamath Proof Explorer

Theorem rngqiprngfulem5

Description: Lemma 5 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 rngqiprngfulem5 
|- ( ph -> ( .1. .x. U ) = .1. )

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 
 |-  ( .1. .x. U ) = ( .1. .x. ( ( E .- ( .1. .x. E ) ) .+ .1. ) )
16 15 a1i 
 |-  ( ph -> ( .1. .x. U ) = ( .1. .x. ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) )
17 1 2 3 4 5 6 7 rngqiprng1elbas 
 |-  ( ph -> .1. e. B )
18 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
19 1 18 syl 
 |-  ( ph -> R e. Grp )
20 1 2 3 4 5 6 7 8 9 10 11 rngqiprngfulem2 
 |-  ( ph -> E e. B )
21 5 6 rngcl 
 |-  ( ( R e. Rng /\ .1. e. B /\ E e. B ) -> ( .1. .x. E ) e. B )
22 1 17 20 21 syl3anc 
 |-  ( ph -> ( .1. .x. E ) e. B )
23 5 12 grpsubcl 
 |-  ( ( R e. Grp /\ E e. B /\ ( .1. .x. E ) e. B ) -> ( E .- ( .1. .x. E ) ) e. B )
24 19 20 22 23 syl3anc 
 |-  ( ph -> ( E .- ( .1. .x. E ) ) e. B )
25 5 13 6 rngdi 
 |-  ( ( R e. Rng /\ ( .1. e. B /\ ( E .- ( .1. .x. E ) ) e. B /\ .1. e. B ) ) -> ( .1. .x. ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) = ( ( .1. .x. ( E .- ( .1. .x. E ) ) ) .+ ( .1. .x. .1. ) ) )
26 1 17 24 17 25 syl13anc 
 |-  ( ph -> ( .1. .x. ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) = ( ( .1. .x. ( E .- ( .1. .x. E ) ) ) .+ ( .1. .x. .1. ) ) )
27 5 6 12 1 17 20 22 rngsubdi 
 |-  ( ph -> ( .1. .x. ( E .- ( .1. .x. E ) ) ) = ( ( .1. .x. E ) .- ( .1. .x. ( .1. .x. E ) ) ) )
28 5 6 rngass 
 |-  ( ( R e. Rng /\ ( .1. e. B /\ .1. e. B /\ E e. B ) ) -> ( ( .1. .x. .1. ) .x. E ) = ( .1. .x. ( .1. .x. E ) ) )
29 1 17 17 20 28 syl13anc 
 |-  ( ph -> ( ( .1. .x. .1. ) .x. E ) = ( .1. .x. ( .1. .x. E ) ) )
30 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
31 2 30 syl 
 |-  ( ph -> .x. = ( .r ` J ) )
32 31 oveqd 
 |-  ( ph -> ( .1. .x. .1. ) = ( .1. ( .r ` J ) .1. ) )
33 eqid 
 |-  ( Base ` J ) = ( Base ` J )
34 33 7 ringidcl 
 |-  ( J e. Ring -> .1. e. ( Base ` J ) )
35 eqid 
 |-  ( .r ` J ) = ( .r ` J )
36 33 35 7 ringlidm 
 |-  ( ( J e. Ring /\ .1. e. ( Base ` J ) ) -> ( .1. ( .r ` J ) .1. ) = .1. )
37 4 34 36 syl2anc2 
 |-  ( ph -> ( .1. ( .r ` J ) .1. ) = .1. )
38 32 37 eqtrd 
 |-  ( ph -> ( .1. .x. .1. ) = .1. )
39 38 oveq1d 
 |-  ( ph -> ( ( .1. .x. .1. ) .x. E ) = ( .1. .x. E ) )
40 29 39 eqtr3d 
 |-  ( ph -> ( .1. .x. ( .1. .x. E ) ) = ( .1. .x. E ) )
41 40 oveq2d 
 |-  ( ph -> ( ( .1. .x. E ) .- ( .1. .x. ( .1. .x. E ) ) ) = ( ( .1. .x. E ) .- ( .1. .x. E ) ) )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 5 42 12 grpsubid 
 |-  ( ( R e. Grp /\ ( .1. .x. E ) e. B ) -> ( ( .1. .x. E ) .- ( .1. .x. E ) ) = ( 0g ` R ) )
44 19 22 43 syl2anc 
 |-  ( ph -> ( ( .1. .x. E ) .- ( .1. .x. E ) ) = ( 0g ` R ) )
45 27 41 44 3eqtrd 
 |-  ( ph -> ( .1. .x. ( E .- ( .1. .x. E ) ) ) = ( 0g ` R ) )
46 45 38 oveq12d 
 |-  ( ph -> ( ( .1. .x. ( E .- ( .1. .x. E ) ) ) .+ ( .1. .x. .1. ) ) = ( ( 0g ` R ) .+ .1. ) )
47 26 46 eqtrd 
 |-  ( ph -> ( .1. .x. ( ( E .- ( .1. .x. E ) ) .+ .1. ) ) = ( ( 0g ` R ) .+ .1. ) )
48 5 13 42 19 17 grplidd 
 |-  ( ph -> ( ( 0g ` R ) .+ .1. ) = .1. )
49 16 47 48 3eqtrd 
 |-  ( ph -> ( .1. .x. U ) = .1. )