Metamath Proof Explorer

Theorem rngqipring1

Description: The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (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. )
rngqipring1.p 
|- P = ( Q Xs. J )
Assertion rngqipring1 
|- ( ph -> ( 1r ` P ) = <. [ E ] .~ , .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 rngqipring1.p 
 |-  P = ( Q Xs. J )
16 15 10 4 xpsring1d 
 |-  ( ph -> ( 1r ` P ) = <. ( 1r ` Q ) , ( 1r ` J ) >. )
17 11 adantr 
 |-  ( ( ph /\ x e. B ) -> E e. ( 1r ` Q ) )
18 eleq2 
 |-  ( ( 1r ` Q ) = [ x ] .~ -> ( E e. ( 1r ` Q ) <-> E e. [ x ] .~ ) )
19 18 adantl 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. ( 1r ` Q ) <-> E e. [ x ] .~ ) )
20 elecg 
 |-  ( ( E e. ( 1r ` Q ) /\ x e. B ) -> ( E e. [ x ] .~ <-> x .~ E ) )
21 11 20 sylan 
 |-  ( ( ph /\ x e. B ) -> ( E e. [ x ] .~ <-> x .~ E ) )
22 ringrng 
 |-  ( J e. Ring -> J e. Rng )
23 4 22 syl 
 |-  ( ph -> J e. Rng )
24 3 23 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
25 1 2 24 rng2idlnsg 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
26 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
27 25 26 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
28 27 adantr 
 |-  ( ( ph /\ x e. B ) -> I e. ( SubGrp ` R ) )
29 5 8 eqger 
 |-  ( I e. ( SubGrp ` R ) -> .~ Er B )
30 28 29 syl 
 |-  ( ( ph /\ x e. B ) -> .~ Er B )
31 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
32 30 31 erth 
 |-  ( ( ph /\ x e. B ) -> ( x .~ E <-> [ x ] .~ = [ E ] .~ ) )
33 32 biimpa 
 |-  ( ( ( ph /\ x e. B ) /\ x .~ E ) -> [ x ] .~ = [ E ] .~ )
34 33 eqcomd 
 |-  ( ( ( ph /\ x e. B ) /\ x .~ E ) -> [ E ] .~ = [ x ] .~ )
35 34 ex 
 |-  ( ( ph /\ x e. B ) -> ( x .~ E -> [ E ] .~ = [ x ] .~ ) )
36 21 35 sylbid 
 |-  ( ( ph /\ x e. B ) -> ( E e. [ x ] .~ -> [ E ] .~ = [ x ] .~ ) )
37 36 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. [ x ] .~ -> [ E ] .~ = [ x ] .~ ) )
38 19 37 sylbid 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( E e. ( 1r ` Q ) -> [ E ] .~ = [ x ] .~ ) )
39 38 ex 
 |-  ( ( ph /\ x e. B ) -> ( ( 1r ` Q ) = [ x ] .~ -> ( E e. ( 1r ` Q ) -> [ E ] .~ = [ x ] .~ ) ) )
40 17 39 mpid 
 |-  ( ( ph /\ x e. B ) -> ( ( 1r ` Q ) = [ x ] .~ -> [ E ] .~ = [ x ] .~ ) )
41 40 imp 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> [ E ] .~ = [ x ] .~ )
42 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> ( 1r ` Q ) = [ x ] .~ )
43 41 42 eqtr4d 
 |-  ( ( ( ph /\ x e. B ) /\ ( 1r ` Q ) = [ x ] .~ ) -> [ E ] .~ = ( 1r ` Q ) )
44 1 2 3 4 5 6 7 8 9 10 rngqiprngfulem1 
 |-  ( ph -> E. x e. B ( 1r ` Q ) = [ x ] .~ )
45 43 44 r19.29a 
 |-  ( ph -> [ E ] .~ = ( 1r ` Q ) )
46 45 eqcomd 
 |-  ( ph -> ( 1r ` Q ) = [ E ] .~ )
47 7 eqcomi 
 |-  ( 1r ` J ) = .1.
48 47 a1i 
 |-  ( ph -> ( 1r ` J ) = .1. )
49 46 48 opeq12d 
 |-  ( ph -> <. ( 1r ` Q ) , ( 1r ` J ) >. = <. [ E ] .~ , .1. >. )
50 16 49 eqtrd 
 |-  ( ph -> ( 1r ` P ) = <. [ E ] .~ , .1. >. )