Metamath Proof Explorer

Theorem qusring2

Description: The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 qusring2.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusring2.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusring2.p 
 |-  .+ = ( +g ` R )
4 qusring2.t 
 |-  .x. = ( .r ` R )
5 qusring2.o 
 |-  .1. = ( 1r ` R )
6 qusring2.r 
 |-  ( ph -> .~ Er V )
7 qusring2.e1 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
8 qusring2.e2 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
9 qusring2.x 
 |-  ( ph -> R e. Ring )
10 eqid 
 |-  ( u e. V |-> [ u ] .~ ) = ( u e. V |-> [ u ] .~ )
11 fvex 
 |-  ( Base ` R ) e. _V
12 2 11 eqeltrdi 
 |-  ( ph -> V e. _V )
13 erex 
 |-  ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
14 6 12 13 sylc 
 |-  ( ph -> .~ e. _V )
15 1 2 10 14 9 qusval 
 |-  ( ph -> U = ( ( u e. V |-> [ u ] .~ ) "s R ) )
16 1 2 10 14 9 quslem 
 |-  ( ph -> ( u e. V |-> [ u ] .~ ) : V -onto-> ( V /. .~ ) )
17 9 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> R e. Ring )
18 simprl 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. V )
19 2 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> V = ( Base ` R ) )
20 18 19 eleqtrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. ( Base ` R ) )
21 simprr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. V )
22 21 19 eleqtrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. ( Base ` R ) )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 23 3 ringacl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) e. ( Base ` R ) )
25 17 20 22 24 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. ( Base ` R ) )
26 25 19 eleqtrrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
27 6 12 10 26 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 .+ b ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( p .+ q ) ) ) )
28 23 4 ringcl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .x. y ) e. ( Base ` R ) )
29 17 20 22 28 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .x. y ) e. ( Base ` R ) )
30 29 19 eleqtrrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .x. y ) e. V )
31 6 12 10 30 8 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 ) ) ) )
32 15 2 3 4 5 16 27 31 9 imasring 
 |-  ( ph -> ( U e. Ring /\ ( ( u e. V |-> [ u ] .~ ) ` .1. ) = ( 1r ` U ) ) )
33 6 12 10 divsfval 
 |-  ( ph -> ( ( u e. V |-> [ u ] .~ ) ` .1. ) = [ .1. ] .~ )
34 33 eqcomd 
 |-  ( ph -> [ .1. ] .~ = ( ( u e. V |-> [ u ] .~ ) ` .1. ) )
35 34 eqeq1d 
 |-  ( ph -> ( [ .1. ] .~ = ( 1r ` U ) <-> ( ( u e. V |-> [ u ] .~ ) ` .1. ) = ( 1r ` U ) ) )
36 35 anbi2d 
 |-  ( ph -> ( ( U e. Ring /\ [ .1. ] .~ = ( 1r ` U ) ) <-> ( U e. Ring /\ ( ( u e. V |-> [ u ] .~ ) ` .1. ) = ( 1r ` U ) ) ) )
37 32 36 mpbird 
 |-  ( ph -> ( U e. Ring /\ [ .1. ] .~ = ( 1r ` U ) ) )