Step |
Hyp |
Ref |
Expression |
1 |
|
quscrng.u |
|- U = ( R /s ( R ~QG S ) ) |
2 |
|
quscrng.i |
|- I = ( LIdeal ` R ) |
3 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
4 |
|
simpr |
|- ( ( R e. CRing /\ S e. I ) -> S e. I ) |
5 |
2
|
crng2idl |
|- ( R e. CRing -> I = ( 2Ideal ` R ) ) |
6 |
5
|
adantr |
|- ( ( R e. CRing /\ S e. I ) -> I = ( 2Ideal ` R ) ) |
7 |
4 6
|
eleqtrd |
|- ( ( R e. CRing /\ S e. I ) -> S e. ( 2Ideal ` R ) ) |
8 |
|
eqid |
|- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
9 |
1 8
|
qusring |
|- ( ( R e. Ring /\ S e. ( 2Ideal ` R ) ) -> U e. Ring ) |
10 |
3 7 9
|
syl2an2r |
|- ( ( R e. CRing /\ S e. I ) -> U e. Ring ) |
11 |
1
|
a1i |
|- ( ( R e. CRing /\ S e. I ) -> U = ( R /s ( R ~QG S ) ) ) |
12 |
|
eqidd |
|- ( ( R e. CRing /\ S e. I ) -> ( Base ` R ) = ( Base ` R ) ) |
13 |
|
ovexd |
|- ( ( R e. CRing /\ S e. I ) -> ( R ~QG S ) e. _V ) |
14 |
3
|
adantr |
|- ( ( R e. CRing /\ S e. I ) -> R e. Ring ) |
15 |
11 12 13 14
|
qusbas |
|- ( ( R e. CRing /\ S e. I ) -> ( ( Base ` R ) /. ( R ~QG S ) ) = ( Base ` U ) ) |
16 |
15
|
eleq2d |
|- ( ( R e. CRing /\ S e. I ) -> ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) <-> x e. ( Base ` U ) ) ) |
17 |
15
|
eleq2d |
|- ( ( R e. CRing /\ S e. I ) -> ( y e. ( ( Base ` R ) /. ( R ~QG S ) ) <-> y e. ( Base ` U ) ) ) |
18 |
16 17
|
anbi12d |
|- ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) <-> ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) ) ) |
19 |
|
eqid |
|- ( ( Base ` R ) /. ( R ~QG S ) ) = ( ( Base ` R ) /. ( R ~QG S ) ) |
20 |
|
oveq2 |
|- ( [ u ] ( R ~QG S ) = y -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( x ( .r ` U ) y ) ) |
21 |
|
oveq1 |
|- ( [ u ] ( R ~QG S ) = y -> ( [ u ] ( R ~QG S ) ( .r ` U ) x ) = ( y ( .r ` U ) x ) ) |
22 |
20 21
|
eqeq12d |
|- ( [ u ] ( R ~QG S ) = y -> ( ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) <-> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) ) |
23 |
|
oveq1 |
|- ( [ v ] ( R ~QG S ) = x -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( x ( .r ` U ) [ u ] ( R ~QG S ) ) ) |
24 |
|
oveq2 |
|- ( [ v ] ( R ~QG S ) = x -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) ) |
25 |
23 24
|
eqeq12d |
|- ( [ v ] ( R ~QG S ) = x -> ( ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) <-> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) ) ) |
26 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
27 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
28 |
26 27
|
crngcom |
|- ( ( R e. CRing /\ u e. ( Base ` R ) /\ v e. ( Base ` R ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) ) |
29 |
28
|
ad4ant134 |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( u ( .r ` R ) v ) = ( v ( .r ` R ) u ) ) |
30 |
29
|
eceq1d |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> [ ( u ( .r ` R ) v ) ] ( R ~QG S ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) ) |
31 |
|
ringrng |
|- ( R e. Ring -> R e. Rng ) |
32 |
3 31
|
syl |
|- ( R e. CRing -> R e. Rng ) |
33 |
32
|
adantr |
|- ( ( R e. CRing /\ S e. I ) -> R e. Rng ) |
34 |
2
|
lidlsubg |
|- ( ( R e. Ring /\ S e. I ) -> S e. ( SubGrp ` R ) ) |
35 |
3 34
|
sylan |
|- ( ( R e. CRing /\ S e. I ) -> S e. ( SubGrp ` R ) ) |
36 |
33 7 35
|
3jca |
|- ( ( R e. CRing /\ S e. I ) -> ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) ) |
37 |
36
|
adantr |
|- ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) -> ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) ) |
38 |
|
simpr |
|- ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) -> u e. ( Base ` R ) ) |
39 |
38
|
anim1i |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( u e. ( Base ` R ) /\ v e. ( Base ` R ) ) ) |
40 |
|
eqid |
|- ( R ~QG S ) = ( R ~QG S ) |
41 |
|
eqid |
|- ( .r ` U ) = ( .r ` U ) |
42 |
40 1 26 27 41
|
qusmulrng |
|- ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( u e. ( Base ` R ) /\ v e. ( Base ` R ) ) ) -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = [ ( u ( .r ` R ) v ) ] ( R ~QG S ) ) |
43 |
37 39 42
|
syl2an2r |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) = [ ( u ( .r ` R ) v ) ] ( R ~QG S ) ) |
44 |
39
|
ancomd |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( v e. ( Base ` R ) /\ u e. ( Base ` R ) ) ) |
45 |
40 1 26 27 41
|
qusmulrng |
|- ( ( ( R e. Rng /\ S e. ( 2Ideal ` R ) /\ S e. ( SubGrp ` R ) ) /\ ( v e. ( Base ` R ) /\ u e. ( Base ` R ) ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) ) |
46 |
37 44 45
|
syl2an2r |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = [ ( v ( .r ` R ) u ) ] ( R ~QG S ) ) |
47 |
30 43 46
|
3eqtr4rd |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ v e. ( Base ` R ) ) -> ( [ v ] ( R ~QG S ) ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) [ v ] ( R ~QG S ) ) ) |
48 |
19 25 47
|
ectocld |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ u e. ( Base ` R ) ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) ) |
49 |
48
|
an32s |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) /\ u e. ( Base ` R ) ) -> ( x ( .r ` U ) [ u ] ( R ~QG S ) ) = ( [ u ] ( R ~QG S ) ( .r ` U ) x ) ) |
50 |
19 22 49
|
ectocld |
|- ( ( ( ( R e. CRing /\ S e. I ) /\ x e. ( ( Base ` R ) /. ( R ~QG S ) ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) |
51 |
50
|
expl |
|- ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( ( Base ` R ) /. ( R ~QG S ) ) /\ y e. ( ( Base ` R ) /. ( R ~QG S ) ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) ) |
52 |
18 51
|
sylbird |
|- ( ( R e. CRing /\ S e. I ) -> ( ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) -> ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) ) |
53 |
52
|
ralrimivv |
|- ( ( R e. CRing /\ S e. I ) -> A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) |
54 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
55 |
54 41
|
iscrng2 |
|- ( U e. CRing <-> ( U e. Ring /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( .r ` U ) y ) = ( y ( .r ` U ) x ) ) ) |
56 |
10 53 55
|
sylanbrc |
|- ( ( R e. CRing /\ S e. I ) -> U e. CRing ) |