drngid2

Description: Properties showing that an element I is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013)

	Ref	Expression
Hypotheses	drngid2.b	$⊢ B = {Base}_{R}$
	drngid2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	drngid2.o	$⊢ \underset{˙}{0} = 0_{R}$
	drngid2.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	drngid2	$⊢ R \in DivRing \to ((I \in B \land I \neq \underset{˙}{0} \land I \underset{˙}{\cdot} I = I) \leftrightarrow \underset{˙}{1} = I)$

Proof

Step	Hyp	Ref	Expression
1		drngid2.b	$⊢ B = {Base}_{R}$
2		drngid2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		drngid2.o	$⊢ \underset{˙}{0} = 0_{R}$
4		drngid2.u	$⊢ \underset{˙}{1} = 1_{R}$
5		df-3an	$⊢ (I \in B \land I \neq \underset{˙}{0} \land I \underset{˙}{\cdot} I = I) \leftrightarrow ((I \in B \land I \neq \underset{˙}{0}) \land I \underset{˙}{\cdot} I = I)$
6		eldifsn	$⊢ I \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (I \in B \land I \neq \underset{˙}{0})$
7	6	anbi1i	$⊢ (I \in (B ∖ \{\underset{˙}{0}\}) \land I \underset{˙}{\cdot} I = I) \leftrightarrow ((I \in B \land I \neq \underset{˙}{0}) \land I \underset{˙}{\cdot} I = I)$
8	5 7	bitr4i	$⊢ (I \in B \land I \neq \underset{˙}{0} \land I \underset{˙}{\cdot} I = I) \leftrightarrow (I \in (B ∖ \{\underset{˙}{0}\}) \land I \underset{˙}{\cdot} I = I)$
9		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
10	1 3 9	drngmgp	$⊢ R \in DivRing \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$
11		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13	12 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
14	9 13	ressbas2	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B \to B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
15	11 14	ax-mp	$⊢ B ∖ \{\underset{˙}{0}\} = {Base}_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
16	1	fvexi	$⊢ B \in V$
17		difexg	$⊢ B \in V \to B ∖ \{\underset{˙}{0}\} \in V$
18	12 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
19	9 18	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
20	16 17 19	mp2b	$⊢ \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
21		eqid	$⊢ 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
22	15 20 21	isgrpid2	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp \to ((I \in (B ∖ \{\underset{˙}{0}\}) \land I \underset{˙}{\cdot} I = I) \leftrightarrow 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = I)$
23	10 22	syl	$⊢ R \in DivRing \to ((I \in (B ∖ \{\underset{˙}{0}\}) \land I \underset{˙}{\cdot} I = I) \leftrightarrow 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = I)$
24	8 23	bitrid	$⊢ R \in DivRing \to ((I \in B \land I \neq \underset{˙}{0} \land I \underset{˙}{\cdot} I = I) \leftrightarrow 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = I)$
25	1 3 4 9	drngid	$⊢ R \in DivRing \to \underset{˙}{1} = 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))}$
26	25	eqeq1d	$⊢ R \in DivRing \to (\underset{˙}{1} = I \leftrightarrow 0_{({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}))} = I)$
27	24 26	bitr4d	$⊢ R \in DivRing \to ((I \in B \land I \neq \underset{˙}{0} \land I \underset{˙}{\cdot} I = I) \leftrightarrow \underset{˙}{1} = I)$

Metamath Proof Explorer

Theorem drngid2

Proof