Metamath Proof Explorer

Theorem quscrng

Description: The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses quscrng.u 
|- U = ( R /s ( R ~QG S ) )
quscrng.i 
|- I = ( LIdeal ` R )
Assertion quscrng 
|- ( ( R e. CRing /\ S e. I ) -> U e. CRing )

Proof

Step Hyp Ref Expression
1 quscrng.u 
 |-  U = ( R /s ( R ~QG S ) )
2 quscrng.i 
 |-  I = ( LIdeal ` R )
3 crngring 
 |-  ( R e. CRing -> R e. Ring )
4 3 adantr 
 |-  ( ( R e. CRing /\ S e. I ) -> R e. Ring )
5 simpr 
 |-  ( ( R e. CRing /\ S e. I ) -> S e. I )
6 2 crng2idl 
 |-  ( R e. CRing -> I = ( 2Ideal ` R ) )
7 6 adantr 
 |-  ( ( R e. CRing /\ S e. I ) -> I = ( 2Ideal ` R ) )
8 5 7 eleqtrd 
 |-  ( ( R e. CRing /\ S e. I ) -> S e. ( 2Ideal ` R ) )
9 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
10 1 9 qusring 
 |-  ( ( R e. Ring /\ S e. ( 2Ideal ` R ) ) -> U e. Ring )
11 4 8 10 syl2anc 
 |-  ( ( R e. CRing /\ S e. I ) -> U e. Ring )
12 1 a1i 
 |-  ( ( R e. CRing /\ S e. I ) -> U = ( R /s ( R ~QG S ) ) )
13 eqidd 
 |-  ( ( R e. CRing /\ S e. I ) -> ( Base ` R ) = ( Base ` R ) )
14 ovexd 
 |-  ( ( R e. CRing /\ S e. I ) -> ( R ~QG S ) e. _V )
15 12 13 14 4 qusbas 
 |-  ( ( R e. CRing /\ S e. I ) -> ( ( Base ` R ) /. ( R ~QG S ) ) = ( Base ` U ) )
16 15 eleq2d 
 |-  ( ( R e. CRing /\ S e. I ) -> ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) <-> x e. ( Base ` U ) ) )
17 15 eleq2d 
 |-  ( ( R e. CRing /\ S e. I ) -> ( y e. ( ( Base ` R ) /. ( R ~QG S ) ) <-> y e. ( Base ` U ) ) )
18 16 17 anbi12d 
 |-  ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) <-> ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) ) )
19 eqid 
 |-  ( ( Base ` R ) /. ( R ~QG S ) ) = ( ( Base ` R ) /. ( R ~QG S ) )
20 oveq2 
 |-  ( [ u ] ( R ~QG S ) = y -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( x ( .r ` U ) y ) )
21 oveq1 
 |-  ( [ u ] ( R ~QG S ) = y -> ( [ u ] ( R ~QG S ) ( .r ` U ) x ) = ( y ( .r ` U ) x ) )
22 20 21 eqeq12d 
 |-  ( [ u ] ( R ~QG S ) = y -> ( ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) <-> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) )
23 oveq1 
 |-  ( [ v ] ( R ~QG S ) = x -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( x ( .r ` U ) [ u ] ( R ~QG S ) ) )
24 oveq2 
 |-  ( [ v ] ( R ~QG S ) = x -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) )
25 23 24 eqeq12d 
 |-  ( [ v ] ( R ~QG S ) = x -> ( ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) <-> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 eqid 
 |-  ( .r ` R ) = ( .r ` R )
28 26 27 crngcom 
 |-  ( ( R e. CRing /\ u e. ( Base ` R ) /\ v e. ( Base ` R ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) )
29 28 ad4ant134 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) )
30 29 eceq1d 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> [ ( u ( .r ` R ) v ) ] ( R ~QG S ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) )
31 2 lidlsubg 
 |-  ( ( R e. Ring /\ S e. I ) -> S e. ( SubGrp ` R ) )
32 3 31 sylan 
 |-  ( ( R e. CRing /\ S e. I ) -> S e. ( SubGrp ` R ) )
33 eqid 
 |-  ( R ~QG S ) = ( R ~QG S )
34 26 33 eqger 
 |-  ( S e. ( SubGrp ` R ) -> ( R ~QG S ) Er ( Base ` R ) )
35 32 34 syl 
 |-  ( ( R e. CRing /\ S e. I ) -> ( R ~QG S ) Er ( Base ` R ) )
36 26 33 9 27 2idlcpbl 
 |-  ( ( R e. Ring /\ S e. ( 2Ideal ` R ) ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( .r ` R ) b ) ( R ~QG S ) ( c ( .r ` R ) d ) ) )
37 4 8 36 syl2anc 
 |-  ( ( R e. CRing /\ S e. I ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( .r ` R ) b ) ( R ~QG S ) ( c ( .r ` R ) d ) ) )
38 26 27 ringcl 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) /\ d e. ( Base ` R ) ) -> ( c ( .r ` R ) d ) e. ( Base ` R ) )
39 38 3expb 
 |-  ( ( R e. Ring /\ ( c e. ( Base ` R ) /\ d e. ( Base ` R ) ) ) -> ( c ( .r ` R ) d ) e. ( Base ` R ) )
40 4 39 sylan 
 |-  ( ( ( R e. CRing /\ S e. I ) /\ ( c e. ( Base ` R ) /\ d e. ( Base ` R ) ) ) -> ( c ( .r ` R ) d ) e. ( Base ` R ) )
41 eqid 
 |-  ( .r ` U ) = ( .r ` U )
42 12 13 35 4 37 40 27 41 qusmulval 
 |-  ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) /\ v e. ( Base ` R ) ) -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = [ ( u ( .r ` R ) v ) ] ( R ~QG S ) )
43 42 3expa 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = [ ( u ( .r ` R ) v ) ] ( R ~QG S ) )
44 12 13 35 4 37 40 27 41 qusmulval 
 |-  ( ( ( R e. CRing /\ S e. I ) /\ v e. ( Base ` R ) /\ u e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) )
45 44 3expa 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ v e. ( Base ` R ) ) /\ u e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) )
46 45 an32s 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) )
47 30 43 46 3eqtr4rd 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) )
48 19 25 47 ectocld 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) )
49 48 an32s 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) /\ u e. ( Base ` R ) ) -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) )
50 19 22 49 ectocld 
 |-  ( ( ( ( R e. CRing /\ S e. I ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) )
51 50 expl 
 |-  ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) )
52 18 51 sylbird 
 |-  ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) )
53 52 ralrimivv 
 |-  ( ( R e. CRing /\ S e. I ) -> A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) )
54 eqid 
 |-  ( Base ` U ) = ( Base ` U )
55 54 41 iscrng2 
 |-  ( U e. CRing <-> ( U e. Ring /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) )
56 11 53 55 sylanbrc 
 |-  ( ( R e. CRing /\ S e. I ) -> U e. CRing )