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