Metamath Proof Explorer

Theorem rngqiprngimfolem

Description: Lemma for rngqiprngimfo . (Contributed by AV, 5-Mar-2025) (Proof shortened by AV, 24-Mar-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
Assertion rngqiprngimfolem 
|- ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( ( C ( -g ` R ) ( .1. .x. C ) ) ( +g ` R ) A ) ) = A )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 1 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> R e. Rng )
9 1 2 3 4 5 6 7 rngqiprng1elbas 
 |-  ( ph -> .1. e. B )
10 9 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> .1. e. B )
11 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
12 1 11 syl 
 |-  ( ph -> R e. Grp )
13 12 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> R e. Grp )
14 simp3 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> C e. B )
15 5 6 rngcl 
 |-  ( ( R e. Rng /\ .1. e. B /\ C e. B ) -> ( .1. .x. C ) e. B )
16 8 10 14 15 syl3anc 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. C ) e. B )
17 eqid 
 |-  ( -g ` R ) = ( -g ` R )
18 5 17 grpsubcl 
 |-  ( ( R e. Grp /\ C e. B /\ ( .1. .x. C ) e. B ) -> ( C ( -g ` R ) ( .1. .x. C ) ) e. B )
19 13 14 16 18 syl3anc 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( C ( -g ` R ) ( .1. .x. C ) ) e. B )
20 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
21 5 20 2idlss 
 |-  ( I e. ( 2Ideal ` R ) -> I C_ B )
22 2 21 syl 
 |-  ( ph -> I C_ B )
23 22 sselda 
 |-  ( ( ph /\ A e. I ) -> A e. B )
24 23 3adant3 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> A e. B )
25 eqid 
 |-  ( +g ` R ) = ( +g ` R )
26 5 25 6 rngdi 
 |-  ( ( R e. Rng /\ ( .1. e. B /\ ( C ( -g ` R ) ( .1. .x. C ) ) e. B /\ A e. B ) ) -> ( .1. .x. ( ( C ( -g ` R ) ( .1. .x. C ) ) ( +g ` R ) A ) ) = ( ( .1. .x. ( C ( -g ` R ) ( .1. .x. C ) ) ) ( +g ` R ) ( .1. .x. A ) ) )
27 8 10 19 24 26 syl13anc 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( ( C ( -g ` R ) ( .1. .x. C ) ) ( +g ` R ) A ) ) = ( ( .1. .x. ( C ( -g ` R ) ( .1. .x. C ) ) ) ( +g ` R ) ( .1. .x. A ) ) )
28 5 6 17 8 10 14 16 rngsubdi 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( C ( -g ` R ) ( .1. .x. C ) ) ) = ( ( .1. .x. C ) ( -g ` R ) ( .1. .x. ( .1. .x. C ) ) ) )
29 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
30 2 29 syl 
 |-  ( ph -> .x. = ( .r ` J ) )
31 30 oveqd 
 |-  ( ph -> ( .1. .x. ( .1. .x. C ) ) = ( .1. ( .r ` J ) ( .1. .x. C ) ) )
32 31 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( .1. .x. C ) ) = ( .1. ( .r ` J ) ( .1. .x. C ) ) )
33 eqid 
 |-  ( Base ` J ) = ( Base ` J )
34 eqid 
 |-  ( .r ` J ) = ( .r ` J )
35 4 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> J e. Ring )
36 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ C e. B ) -> ( .1. .x. C ) e. ( Base ` J ) )
37 36 3adant2 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. C ) e. ( Base ` J ) )
38 33 34 7 35 37 ringlidmd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. ( .r ` J ) ( .1. .x. C ) ) = ( .1. .x. C ) )
39 32 38 eqtrd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( .1. .x. C ) ) = ( .1. .x. C ) )
40 39 oveq2d 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( ( .1. .x. C ) ( -g ` R ) ( .1. .x. ( .1. .x. C ) ) ) = ( ( .1. .x. C ) ( -g ` R ) ( .1. .x. C ) ) )
41 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
42 5 41 17 grpsubid 
 |-  ( ( R e. Grp /\ ( .1. .x. C ) e. B ) -> ( ( .1. .x. C ) ( -g ` R ) ( .1. .x. C ) ) = ( 0g ` R ) )
43 13 16 42 syl2anc 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( ( .1. .x. C ) ( -g ` R ) ( .1. .x. C ) ) = ( 0g ` R ) )
44 28 40 43 3eqtrd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( C ( -g ` R ) ( .1. .x. C ) ) ) = ( 0g ` R ) )
45 44 oveq1d 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( ( .1. .x. ( C ( -g ` R ) ( .1. .x. C ) ) ) ( +g ` R ) ( .1. .x. A ) ) = ( ( 0g ` R ) ( +g ` R ) ( .1. .x. A ) ) )
46 5 6 rngcl 
 |-  ( ( R e. Rng /\ .1. e. B /\ A e. B ) -> ( .1. .x. A ) e. B )
47 8 10 24 46 syl3anc 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. A ) e. B )
48 5 25 41 13 47 grplidd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( ( 0g ` R ) ( +g ` R ) ( .1. .x. A ) ) = ( .1. .x. A ) )
49 30 oveqd 
 |-  ( ph -> ( .1. .x. A ) = ( .1. ( .r ` J ) A ) )
50 49 3ad2ant1 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. A ) = ( .1. ( .r ` J ) A ) )
51 4 adantr 
 |-  ( ( ph /\ A e. I ) -> J e. Ring )
52 2 3 33 2idlbas 
 |-  ( ph -> ( Base ` J ) = I )
53 52 eqcomd 
 |-  ( ph -> I = ( Base ` J ) )
54 53 eleq2d 
 |-  ( ph -> ( A e. I <-> A e. ( Base ` J ) ) )
55 54 biimpa 
 |-  ( ( ph /\ A e. I ) -> A e. ( Base ` J ) )
56 33 34 7 51 55 ringlidmd 
 |-  ( ( ph /\ A e. I ) -> ( .1. ( .r ` J ) A ) = A )
57 56 3adant3 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. ( .r ` J ) A ) = A )
58 48 50 57 3eqtrd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( ( 0g ` R ) ( +g ` R ) ( .1. .x. A ) ) = A )
59 27 45 58 3eqtrd 
 |-  ( ( ph /\ A e. I /\ C e. B ) -> ( .1. .x. ( ( C ( -g ` R ) ( .1. .x. C ) ) ( +g ` R ) A ) ) = A )