This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = ( 𝑅 /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 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ 𝐼 )
5 2 crng2idl ⊢ ( 𝑅 ∈ CRing → 𝐼 = ( 2Ideal ‘ 𝑅 ) )
6 5 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝐼 = ( 2Ideal ‘ 𝑅 ) )
7 4 6 eleqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) )
8 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
9 1 8 qusring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑈 ∈ Ring )
10 3 7 9 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑈 ∈ Ring )
11 1 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) ) )
12 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
13 ovexd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → ( 𝑅 ~QG 𝑆 ) ∈ V )
14 3 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Ring )
15 11 12 13 14 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 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
32 3 31 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Rng )
33 32 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑅 ∈ Rng )
34 2 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
35 3 34 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
36 33 7 35 3jca ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) )
37 36 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) )
38 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
39 38 anim1i ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) )
40 eqid ⊢ ( 𝑅 ~QG 𝑆 ) = ( 𝑅 ~QG 𝑆 )
41 eqid ⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
42 40 1 26 27 41 qusmulrng ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) ) → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) ] ( 𝑅 ~QG 𝑆 ) )
43 37 39 42 syl2an2r ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑢 ( .r ‘ 𝑅 ) 𝑣 ) ] ( 𝑅 ~QG 𝑆 ) )
44 39 ancomd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑣 ∈ ( Base ‘ 𝑅 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) )
45 40 1 26 27 41 qusmulrng ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑅 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) ) → ( [ 𝑣 ] ( 𝑅 ~QG 𝑆 ) ( .r ‘ 𝑈 ) [ 𝑢 ] ( 𝑅 ~QG 𝑆 ) ) = [ ( 𝑣 ( .r ‘ 𝑅 ) 𝑢 ) ] ( 𝑅 ~QG 𝑆 ) )
46 37 44 45 syl2an2r ⊢ ( ( ( ( 𝑅 ∈ 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 10 53 55 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ 𝐼 ) → 𝑈 ∈ CRing )