Metamath Proof Explorer

Theorem rngqiprngghm

Description: F is a homomorphism of the additive groups of non-unital rings. (Contributed by AV, 24-Feb-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 )
rngqiprngim.g 
|- .~ = ( R ~QG I )
rngqiprngim.q 
|- Q = ( R /s .~ )
rngqiprngim.c 
|- C = ( Base ` Q )
rngqiprngim.p 
|- P = ( Q Xs. J )
rngqiprngim.f 
|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
Assertion rngqiprngghm 
|- ( ph -> F e. ( R GrpHom P ) )

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 rngqiprngim.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngim.q 
 |-  Q = ( R /s .~ )
10 rngqiprngim.c 
 |-  C = ( Base ` Q )
11 rngqiprngim.p 
 |-  P = ( Q Xs. J )
12 rngqiprngim.f 
 |-  F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
13 eqid 
 |-  ( Base ` P ) = ( Base ` P )
14 eqid 
 |-  ( +g ` R ) = ( +g ` R )
15 eqid 
 |-  ( +g ` P ) = ( +g ` P )
16 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
17 1 16 syl 
 |-  ( ph -> R e. Grp )
18 1 2 3 4 5 6 7 8 9 10 11 rngqiprng 
 |-  ( ph -> P e. Rng )
19 rnggrp 
 |-  ( P e. Rng -> P e. Grp )
20 18 19 syl 
 |-  ( ph -> P e. Grp )
21 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimf 
 |-  ( ph -> F : B --> ( C X. I ) )
22 1 2 3 4 5 6 7 8 9 10 11 rngqipbas 
 |-  ( ph -> ( Base ` P ) = ( C X. I ) )
23 22 feq3d 
 |-  ( ph -> ( F : B --> ( Base ` P ) <-> F : B --> ( C X. I ) ) )
24 21 23 mpbird 
 |-  ( ph -> F : B --> ( Base ` P ) )
25 ringrng 
 |-  ( J e. Ring -> J e. Rng )
26 4 25 syl 
 |-  ( ph -> J e. Rng )
27 3 26 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
28 1 2 27 rng2idlnsg 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
29 28 5 8 9 ecqusaddd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ ( a ( +g ` R ) b ) ] .~ = ( [ a ] .~ ( +g ` Q ) [ b ] .~ ) )
30 1 2 3 4 5 6 7 rngqiprngghmlem3 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .1. .x. ( a ( +g ` R ) b ) ) = ( ( .1. .x. a ) ( +g ` J ) ( .1. .x. b ) ) )
31 29 30 opeq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> <. [ ( a ( +g ` R ) b ) ] .~ , ( .1. .x. ( a ( +g ` R ) b ) ) >. = <. ( [ a ] .~ ( +g ` Q ) [ b ] .~ ) , ( ( .1. .x. a ) ( +g ` J ) ( .1. .x. b ) ) >. )
32 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
33 eqid 
 |-  ( Base ` J ) = ( Base ` J )
34 9 ovexi 
 |-  Q e. _V
35 34 a1i 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> Q e. _V )
36 4 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> J e. Ring )
37 simpl 
 |-  ( ( a e. B /\ b e. B ) -> a e. B )
38 8 9 5 32 quseccl0 
 |-  ( ( R e. Rng /\ a e. B ) -> [ a ] .~ e. ( Base ` Q ) )
39 1 37 38 syl2an 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ a ] .~ e. ( Base ` Q ) )
40 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ a e. B ) -> ( .1. .x. a ) e. ( Base ` J ) )
41 40 adantrr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .1. .x. a ) e. ( Base ` J ) )
42 simpr 
 |-  ( ( a e. B /\ b e. B ) -> b e. B )
43 8 9 5 32 quseccl0 
 |-  ( ( R e. Rng /\ b e. B ) -> [ b ] .~ e. ( Base ` Q ) )
44 1 42 43 syl2an 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> [ b ] .~ e. ( Base ` Q ) )
45 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ b e. B ) -> ( .1. .x. b ) e. ( Base ` J ) )
46 45 adantrl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( .1. .x. b ) e. ( Base ` J ) )
47 28 5 8 9 ecqusaddcl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( [ a ] .~ ( +g ` Q ) [ b ] .~ ) e. ( Base ` Q ) )
48 1 2 3 4 5 6 7 rngqiprngghmlem2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( .1. .x. a ) ( +g ` J ) ( .1. .x. b ) ) e. ( Base ` J ) )
49 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
50 eqid 
 |-  ( +g ` J ) = ( +g ` J )
51 11 32 33 35 36 39 41 44 46 47 48 49 50 15 xpsadd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( <. [ a ] .~ , ( .1. .x. a ) >. ( +g ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) = <. ( [ a ] .~ ( +g ` Q ) [ b ] .~ ) , ( ( .1. .x. a ) ( +g ` J ) ( .1. .x. b ) ) >. )
52 31 51 eqtr4d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> <. [ ( a ( +g ` R ) b ) ] .~ , ( .1. .x. ( a ( +g ` R ) b ) ) >. = ( <. [ a ] .~ , ( .1. .x. a ) >. ( +g ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) )
53 1 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> R e. Rng )
54 37 adantl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. B )
55 42 adantl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. B )
56 5 14 rngacl 
 |-  ( ( R e. Rng /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )
57 53 54 55 56 syl3anc 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
58 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ ( a ( +g ` R ) b ) e. B ) -> ( F ` ( a ( +g ` R ) b ) ) = <. [ ( a ( +g ` R ) b ) ] .~ , ( .1. .x. ( a ( +g ` R ) b ) ) >. )
59 57 58 syldan 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` R ) b ) ) = <. [ ( a ( +g ` R ) b ) ] .~ , ( .1. .x. ( a ( +g ` R ) b ) ) >. )
60 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
61 60 adantrr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
62 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ b e. B ) -> ( F ` b ) = <. [ b ] .~ , ( .1. .x. b ) >. )
63 62 adantrl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) = <. [ b ] .~ , ( .1. .x. b ) >. )
64 61 63 oveq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( +g ` P ) ( F ` b ) ) = ( <. [ a ] .~ , ( .1. .x. a ) >. ( +g ` P ) <. [ b ] .~ , ( .1. .x. b ) >. ) )
65 52 59 64 3eqtr4d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( ( F ` a ) ( +g ` P ) ( F ` b ) ) )
66 5 13 14 15 17 20 24 65 isghmd 
 |-  ( ph -> F e. ( R GrpHom P ) )