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 = {mulGrp}_{R} ↾_{𝑠} A$
	ringidss.b	$⊢ B = {Base}_{R}$
	ringidss.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	ringidss	$⊢ (R \in Ring \land A \subseteq B \land \underset{˙}{1} \in A) \to \underset{˙}{1} = 0_{M}$

Proof

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

Metamath Proof Explorer

Theorem ringidss

Proof