Metamath Proof Explorer

Theorem qus1

Description: The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses qusring.u 
|- U = ( R /s ( R ~QG S ) )
qusring.i 
|- I = ( 2Ideal ` R )
qus1.o 
|- .1. = ( 1r ` R )
Assertion qus1 
|- ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ .1. ] ( R ~QG S ) = ( 1r ` U ) ) )

Proof

Step Hyp Ref Expression
1 qusring.u 
 |-  U = ( R /s ( R ~QG S ) )
2 qusring.i 
 |-  I = ( 2Ideal ` R )
3 qus1.o 
 |-  .1. = ( 1r ` R )
4 1 a1i 
 |-  ( ( R e. Ring /\ S e. I ) -> U = ( R /s ( R ~QG S ) ) )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 a1i 
 |-  ( ( R e. Ring /\ S e. I ) -> ( Base ` R ) = ( Base ` R ) )
7 eqid 
 |-  ( +g ` R ) = ( +g ` R )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
10 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
11 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
12 9 10 11 2 2idlval 
 |-  I = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) )
13 12 elin2 
 |-  ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
14 13 simplbi 
 |-  ( S e. I -> S e. ( LIdeal ` R ) )
15 9 lidlsubg 
 |-  ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) -> S e. ( SubGrp ` R ) )
16 14 15 sylan2 
 |-  ( ( R e. Ring /\ S e. I ) -> S e. ( SubGrp ` R ) )
17 eqid 
 |-  ( R ~QG S ) = ( R ~QG S )
18 5 17 eqger 
 |-  ( S e. ( SubGrp ` R ) -> ( R ~QG S ) Er ( Base ` R ) )
19 16 18 syl 
 |-  ( ( R e. Ring /\ S e. I ) -> ( R ~QG S ) Er ( Base ` R ) )
20 ringabl 
 |-  ( R e. Ring -> R e. Abel )
21 20 adantr 
 |-  ( ( R e. Ring /\ S e. I ) -> R e. Abel )
22 ablnsg 
 |-  ( R e. Abel -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
23 21 22 syl 
 |-  ( ( R e. Ring /\ S e. I ) -> ( NrmSGrp ` R ) = ( SubGrp ` R ) )
24 16 23 eleqtrrd 
 |-  ( ( R e. Ring /\ S e. I ) -> S e. ( NrmSGrp ` R ) )
25 5 17 7 eqgcpbl 
 |-  ( S e. ( NrmSGrp ` R ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( +g ` R ) b ) ( R ~QG S ) ( c ( +g ` R ) d ) ) )
26 24 25 syl 
 |-  ( ( R e. Ring /\ S e. I ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( +g ` R ) b ) ( R ~QG S ) ( c ( +g ` R ) d ) ) )
27 5 17 2 8 2idlcpbl 
 |-  ( ( R e. Ring /\ S e. I ) -> ( ( a ( R ~QG S ) c /\ b ( R ~QG S ) d ) -> ( a ( .r ` R ) b ) ( R ~QG S ) ( c ( .r ` R ) d ) ) )
28 simpl 
 |-  ( ( R e. Ring /\ S e. I ) -> R e. Ring )
29 4 6 7 8 3 19 26 27 28 qusring2 
 |-  ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ .1. ] ( R ~QG S ) = ( 1r ` U ) ) )