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	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	qus1	$⊢ (R \in Ring \land S \in I) \to (U \in Ring \land [\underset{˙}{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	$⊢ \underset{˙}{1} = 1_{R}$
4	1	a1i	$⊢ (R \in Ring \land S \in I) \to U = R /_{𝑠} (R ~_{QG} S)$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5	a1i	$⊢ (R \in Ring \land S \in I) \to {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ +_{R} = +_{R}$
8		eqid	$⊢ \cdot_{R} = \cdot_{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) \cap LIdeal ({opp}_{r} (R))$
13	12	elin2	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
14	13	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
15	9	lidlsubg	$⊢ (R \in Ring \land S \in LIdeal (R)) \to S \in SubGrp (R)$
16	14 15	sylan2	$⊢ (R \in Ring \land S \in I) \to S \in SubGrp (R)$
17		eqid	$⊢ R ~_{QG} S = R ~_{QG} S$
18	5 17	eqger	$⊢ S \in SubGrp (R) \to (R ~_{QG} S) Er {Base}_{R}$
19	16 18	syl	$⊢ (R \in Ring \land S \in I) \to (R ~_{QG} S) Er {Base}_{R}$
20		ringabl	$⊢ R \in Ring \to R \in Abel$
21	20	adantr	$⊢ (R \in Ring \land S \in I) \to R \in Abel$
22		ablnsg	$⊢ R \in Abel \to NrmSGrp (R) = SubGrp (R)$
23	21 22	syl	$⊢ (R \in Ring \land S \in I) \to NrmSGrp (R) = SubGrp (R)$
24	16 23	eleqtrrd	$⊢ (R \in Ring \land S \in I) \to S \in NrmSGrp (R)$
25	5 17 7	eqgcpbl	$⊢ S \in NrmSGrp (R) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a +_{R} b) (R ~_{QG} S) (c +_{R} d))$
26	24 25	syl	$⊢ (R \in Ring \land S \in I) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a +_{R} b) (R ~_{QG} S) (c +_{R} d))$
27	5 17 2 8	2idlcpbl	$⊢ (R \in Ring \land S \in I) \to ((a (R ~_{QG} S) c \land b (R ~_{QG} S) d) \to (a \cdot_{R} b) (R ~_{QG} S) (c \cdot_{R} d))$
28		simpl	$⊢ (R \in Ring \land S \in I) \to R \in Ring$
29	4 6 7 8 3 19 26 27 28	qusring2	$⊢ (R \in Ring \land S \in I) \to (U \in Ring \land [\underset{˙}{1}] (R ~_{QG} S) = 1_{U})$

Metamath Proof Explorer

Theorem qus1

Proof