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) (Proof shortened by AV, 3-Apr-2025)

Ref Expression
Hypotheses quscrng.u U = R / 𝑠 R ~ QG S
quscrng.i I = LIdeal R
Assertion quscrng R CRing S I U CRing

Proof

Step Hyp Ref Expression
1 quscrng.u U = R / 𝑠 R ~ QG S
2 quscrng.i I = LIdeal R
3 crngring R CRing R Ring
4 simpr R CRing S I S I
5 2 crng2idl R CRing I = 2Ideal R
6 5 adantr R CRing S I I = 2Ideal R
7 4 6 eleqtrd R CRing S I S 2Ideal R
8 eqid 2Ideal R = 2Ideal R
9 1 8 qusring R Ring S 2Ideal R U Ring
10 3 7 9 syl2an2r R CRing S I U Ring
11 1 a1i R CRing S I U = R / 𝑠 R ~ QG S
12 eqidd R CRing S I Base R = Base R
13 ovexd R CRing S I R ~ QG S V
14 3 adantr R CRing S I R Ring
15 11 12 13 14 qusbas R CRing S I Base R / R ~ QG S = Base U
16 15 eleq2d R CRing S I x Base R / R ~ QG S x Base U
17 15 eleq2d R CRing S I y Base R / R ~ QG S y Base U
18 16 17 anbi12d R CRing S I x Base R / R ~ QG S y Base R / R ~ QG S x Base U y Base U
19 eqid Base R / R ~ QG S = Base R / R ~ QG S
20 oveq2 u R ~ QG S = y x U u R ~ QG S = x U y
21 oveq1 u R ~ QG S = y u R ~ QG S U x = y U x
22 20 21 eqeq12d u R ~ QG S = y x U u R ~ QG S = u R ~ QG S U x x U y = y U x
23 oveq1 v R ~ QG S = x v R ~ QG S U u R ~ QG S = x U u R ~ QG S
24 oveq2 v R ~ QG S = x u R ~ QG S U v R ~ QG S = u R ~ QG S U x
25 23 24 eqeq12d v R ~ QG S = x v R ~ QG S U u R ~ QG S = u R ~ QG S U v R ~ QG S x U u R ~ QG S = u R ~ QG S U x
26 eqid Base R = Base R
27 eqid R = R
28 26 27 crngcom R CRing u Base R v Base R u R v = v R u
29 28 ad4ant134 R CRing S I u Base R v Base R u R v = v R u
30 29 eceq1d R CRing S I u Base R v Base R u R v R ~ QG S = v R u R ~ QG S
31 ringrng R Ring R Rng
32 3 31 syl R CRing R Rng
33 32 adantr R CRing S I R Rng
34 2 lidlsubg R Ring S I S SubGrp R
35 3 34 sylan R CRing S I S SubGrp R
36 33 7 35 3jca R CRing S I R Rng S 2Ideal R S SubGrp R
37 36 adantr R CRing S I u Base R R Rng S 2Ideal R S SubGrp R
38 simpr R CRing S I u Base R u Base R
39 38 anim1i R CRing S I u Base R v Base R u Base R v Base R
40 eqid R ~ QG S = R ~ QG S
41 eqid U = U
42 40 1 26 27 41 qusmulrng R Rng S 2Ideal R S SubGrp R u Base R v Base R u R ~ QG S U v R ~ QG S = u R v R ~ QG S
43 37 39 42 syl2an2r R CRing S I u Base R v Base R u R ~ QG S U v R ~ QG S = u R v R ~ QG S
44 39 ancomd R CRing S I u Base R v Base R v Base R u Base R
45 40 1 26 27 41 qusmulrng R Rng S 2Ideal R S SubGrp R v Base R u Base R v R ~ QG S U u R ~ QG S = v R u R ~ QG S
46 37 44 45 syl2an2r R CRing S I u Base R v Base R v R ~ QG S U u R ~ QG S = v R u R ~ QG S
47 30 43 46 3eqtr4rd R CRing S I u Base R v Base R v R ~ QG S U u R ~ QG S = u R ~ QG S U v R ~ QG S
48 19 25 47 ectocld R CRing S I u Base R x Base R / R ~ QG S x U u R ~ QG S = u R ~ QG S U x
49 48 an32s R CRing S I x Base R / R ~ QG S u Base R x U u R ~ QG S = u R ~ QG S U x
50 19 22 49 ectocld R CRing S I x Base R / R ~ QG S y Base R / R ~ QG S x U y = y U x
51 50 expl R CRing S I x Base R / R ~ QG S y Base R / R ~ QG S x U y = y U x
52 18 51 sylbird R CRing S I x Base U y Base U x U y = y U x
53 52 ralrimivv R CRing S I x Base U y Base U x U y = y U x
54 eqid Base U = Base U
55 54 41 iscrng2 U CRing U Ring x Base U y Base U x U y = y U x
56 10 53 55 sylanbrc R CRing S I U CRing