Theorem ringidss

Description: A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	ringidss.g	$$⊢M={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}A$$
	ringidss.b	$$⊢B={\mathrm{Base}}_R$$
	ringidss.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringidss	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to \underset{\dot{}}{1}=0_M$$

Proof

Step	Hyp	Ref	Expression
1		ringidss.g	$$⊢M={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}A$$
2		ringidss.b	$$⊢B={\mathrm{Base}}_R$$
3		ringidss.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
5		eqid	$$⊢0_M=0_M$$
6		eqid	$$⊢{+}_M={+}_M$$
7		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to \underset{\dot{}}{1}\in A$$
8		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
9	8 2	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
10	1 9	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_M$$
11	10	3ad2ant2	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to A={\mathrm{Base}}_M$$
12	7 11	eleqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_M$$
13		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to A\subseteq B$$
14	11 13	eqsstrrd	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to {\mathrm{Base}}_M\subseteq B$$
15	14	sselda	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in {\mathrm{Base}}_M\right)\to y\in B$$
16		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
17	11 16	eqeltrdi	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to A\in \mathrm{V}$$
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	8 18	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
20	1 19	ressplusg	$$⊢A\in \mathrm{V}\to {\cdot }_R={+}_M$$
21	17 20	syl	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to {\cdot }_R={+}_M$$
22	21	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to {\cdot }_R={+}_M$$
23	22	oveqd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to \underset{\dot{}}{1}{\cdot }_{R}y=\underset{\dot{}}{1}{+}_{M}y$$
24	2 18 3	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge y\in B\right)\to \underset{\dot{}}{1}{\cdot }_{R}y=y$$
25	24	3ad2antl1	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to \underset{\dot{}}{1}{\cdot }_{R}y=y$$
26	23 25	eqtr3d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to \underset{\dot{}}{1}{+}_{M}y=y$$
27	15 26	syldan	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in {\mathrm{Base}}_M\right)\to \underset{\dot{}}{1}{+}_{M}y=y$$
28	22	oveqd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to y{\cdot }_R\underset{\dot{}}{1}=y{+}_M\underset{\dot{}}{1}$$
29	2 18 3	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge y\in B\right)\to y{\cdot }_R\underset{\dot{}}{1}=y$$
30	29	3ad2antl1	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to y{\cdot }_R\underset{\dot{}}{1}=y$$
31	28 30	eqtr3d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in B\right)\to y{+}_M\underset{\dot{}}{1}=y$$
32	15 31	syldan	$$⊢\left(\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\wedge y\in {\mathrm{Base}}_M\right)\to y{+}_M\underset{\dot{}}{1}=y$$
33	4 5 6 12 27 32	ismgmid2	$$⊢\left(R\in \mathrm{Ring}\wedge A\subseteq B\wedge \underset{\dot{}}{1}\in A\right)\to \underset{\dot{}}{1}=0_M$$