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 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
quscrng.i 𝐼 = ( LIdeal ‘ 𝑅 )
Assertion quscrng ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑈 ∈ CRing )

Proof

Step Hyp Ref Expression
1 quscrng.u 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
2 quscrng.i 𝐼 = ( LIdeal ‘ 𝑅 )
3 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
4 3 adantr ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑅 ∈ Ring )
5 simpr ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑆𝐼 )
6 2 crng2idl ( 𝑅 ∈ CRing → 𝐼 = ( 2Ideal ‘ 𝑅 ) )
7 6 adantr ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝐼 = ( 2Ideal ‘ 𝑅 ) )
8 5 7 eleqtrd ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) )
9 eqid ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
10 1 9 qusring ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑈 ∈ Ring )
11 4 8 10 syl2anc ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑈 ∈ Ring )
12 1 a1i ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) ) )
13 eqidd ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
14 ovexd ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( 𝑅 ~QG 𝑆 ) ∈ V )
15 12 13 14 4 qusbas ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) = ( Base ‘ 𝑈 ) )
16 15 eleq2d ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝑈 ) ) )
17 15 eleq2d ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ↔ 𝑦 ∈ ( Base ‘ 𝑈 ) ) )
18 16 17 anbi12d ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ) )
19 eqid ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) = ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) )
20 oveq2 ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) = 𝑦 → ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( 𝑥 ( .r𝑈 ) 𝑦 ) )
21 oveq1 ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) = 𝑦 → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) )
22 20 21 eqeq12d ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) = 𝑦 → ( ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) ↔ ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) ) )
23 oveq1 ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) = 𝑥 → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) )
24 oveq2 ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) = 𝑥 → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) )
25 23 24 eqeq12d ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) = 𝑥 → ( ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) ↔ ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) ) )
26 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 eqid ( .r𝑅 ) = ( .r𝑅 )
28 26 27 crngcom ( ( 𝑅 ∈ CRing ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ( .r𝑅 ) 𝑣 ) = ( 𝑣 ( .r𝑅 ) 𝑢 ) )
29 28 ad4ant134 ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ( .r𝑅 ) 𝑣 ) = ( 𝑣 ( .r𝑅 ) 𝑢 ) )
30 29 eceq1d ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → [ ( 𝑢 ( .r𝑅 ) 𝑣 ) ] ( 𝑅 ~QG 𝑆 ) = [ ( 𝑣 ( .r𝑅 ) 𝑢 ) ] ( 𝑅 ~QG 𝑆 ) )
31 2 lidlsubg ( ( 𝑅 ∈ Ring ∧ 𝑆𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
32 3 31 sylan ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
33 eqid ( 𝑅 ~QG 𝑆 ) = ( 𝑅 ~QG 𝑆 )
34 26 33 eqger ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
35 32 34 syl ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( 𝑅 ~QG 𝑆 ) Er ( Base ‘ 𝑅 ) )
36 26 33 9 27 2idlcpbl ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( .r𝑅 ) 𝑑 ) ) )
37 4 8 36 syl2anc ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( ( 𝑎 ( 𝑅 ~QG 𝑆 ) 𝑐𝑏 ( 𝑅 ~QG 𝑆 ) 𝑑 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ( 𝑅 ~QG 𝑆 ) ( 𝑐 ( .r𝑅 ) 𝑑 ) ) )
38 26 27 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑐 ( .r𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
39 38 3expb ( ( 𝑅 ∈ Ring ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑐 ( .r𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
40 4 39 sylan ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑐 ( .r𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
41 eqid ( .r𝑈 ) = ( .r𝑈 )
42 12 13 35 4 37 40 27 41 qusmulval ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑢 ( .r𝑅 ) 𝑣 ) ] ( 𝑅 ~QG 𝑆 ) )
43 42 3expa ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑢 ( .r𝑅 ) 𝑣 ) ] ( 𝑅 ~QG 𝑆 ) )
44 12 13 35 4 37 40 27 41 qusmulval ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑣 ( .r𝑅 ) 𝑢 ) ] ( 𝑅 ~QG 𝑆 ) )
45 44 3expa ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑣 ( .r𝑅 ) 𝑢 ) ] ( 𝑅 ~QG 𝑆 ) )
46 45 an32s ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑣 ( .r𝑅 ) 𝑢 ) ] ( 𝑅 ~QG 𝑆 ) )
47 30 43 46 3eqtr4rd ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) )
48 19 25 47 ectocld ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) → ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) )
49 48 an32s ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r𝑈 ) 𝑥 ) )
50 19 22 49 ectocld ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) → ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) )
51 50 expl ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑆 ) ) ) → ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) ) )
52 18 51 sylbird ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) ) )
53 52 ralrimivv ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) )
54 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
55 54 41 iscrng2 ( 𝑈 ∈ CRing ↔ ( 𝑈 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( .r𝑈 ) 𝑦 ) = ( 𝑦 ( .r𝑈 ) 𝑥 ) ) )
56 11 53 55 sylanbrc ( ( 𝑅 ∈ CRing ∧ 𝑆𝐼 ) → 𝑈 ∈ CRing )