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 )