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 ) |