This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusrng

Description: The quotient structure of a non-unital ring is a non-unital ring ( qusring2 analog). (Contributed by AV, 23-Feb-2025)

Ref Expression
Hypotheses qusrng.u 
|- ( ph -> U = ( R /s .~ ) )
qusrng.v 
|- ( ph -> V = ( Base ` R ) )
qusrng.p 
|- .+ = ( +g ` R )
qusrng.t 
|- .x. = ( .r ` R )
qusrng.r 
|- ( ph -> .~ Er V )
qusrng.e1 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
qusrng.e2 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
qusrng.x 
|- ( ph -> R e. Rng )
Assertion qusrng 
|- ( ph -> U e. Rng )

Proof

Step Hyp Ref Expression
1 qusrng.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusrng.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusrng.p 
 |-  .+ = ( +g ` R )
4 qusrng.t 
 |-  .x. = ( .r ` R )
5 qusrng.r 
 |-  ( ph -> .~ Er V )
6 qusrng.e1 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
7 qusrng.e2 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
8 qusrng.x 
 |-  ( ph -> R e. Rng )
9 eqid 
 |-  ( u e. V |-> [ u ] .~ ) = ( u e. V |-> [ u ] .~ )
10 fvex 
 |-  ( Base ` R ) e. _V
11 2 10 eqeltrdi 
 |-  ( ph -> V e. _V )
12 erex 
 |-  ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
13 5 11 12 sylc 
 |-  ( ph -> .~ e. _V )
14 1 2 9 13 8 qusval 
 |-  ( ph -> U = ( ( u e. V |-> [ u ] .~ ) "s R ) )
15 1 2 9 13 8 quslem 
 |-  ( ph -> ( u e. V |-> [ u ] .~ ) : V -onto-> ( V /. .~ ) )
16 8 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> R e. Rng )
17 simprl 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. V )
18 2 eleq2d 
 |-  ( ph -> ( x e. V <-> x e. ( Base ` R ) ) )
19 18 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x e. V <-> x e. ( Base ` R ) ) )
20 17 19 mpbid 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. ( Base ` R ) )
21 simprr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. V )
22 2 eleq2d 
 |-  ( ph -> ( y e. V <-> y e. ( Base ` R ) ) )
23 22 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( y e. V <-> y e. ( Base ` R ) ) )
24 21 23 mpbid 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. ( Base ` R ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 25 3 rngacl 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) e. ( Base ` R ) )
27 16 20 24 26 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. ( Base ` R ) )
28 2 eleq2d 
 |-  ( ph -> ( ( x .+ y ) e. V <-> ( x .+ y ) e. ( Base ` R ) ) )
29 28 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( ( x .+ y ) e. V <-> ( x .+ y ) e. ( Base ` R ) ) )
30 27 29 mpbird 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
31 5 11 9 30 6 ercpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( ( u e. V |-> [ u ] .~ ) ` a ) = ( ( u e. V |-> [ u ] .~ ) ` p ) /\ ( ( u e. V |-> [ u ] .~ ) ` b ) = ( ( u e. V |-> [ u ] .~ ) ` q ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( a .+ b ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( p .+ q ) ) ) )
32 25 4 rngcl 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .x. y ) e. ( Base ` R ) )
33 16 20 24 32 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .x. y ) e. ( Base ` R ) )
34 2 eleq2d 
 |-  ( ph -> ( ( x .x. y ) e. V <-> ( x .x. y ) e. ( Base ` R ) ) )
35 34 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( ( x .x. y ) e. V <-> ( x .x. y ) e. ( Base ` R ) ) )
36 33 35 mpbird 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .x. y ) e. V )
37 5 11 9 36 7 ercpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( ( u e. V |-> [ u ] .~ ) ` a ) = ( ( u e. V |-> [ u ] .~ ) ` p ) /\ ( ( u e. V |-> [ u ] .~ ) ` b ) = ( ( u e. V |-> [ u ] .~ ) ` q ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( a .x. b ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( p .x. q ) ) ) )
38 14 2 3 4 15 31 37 8 imasrng 
 |-  ( ph -> U e. Rng )