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 / 𝑠 R ~ QG S
qusring.i I = 2Ideal R
qus1.o 1 ˙ = 1 R
Assertion qus1 R Ring S I U Ring 1 ˙ R ~ QG S = 1 U

Proof

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