unitrrg

Description: Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypotheses	unitrrg.e	$⊢ E = RLReg (R)$
	unitrrg.u	$⊢ U = Unit (R)$
Assertion	unitrrg	$⊢ R \in Ring \to U \subseteq E$

Proof

Step	Hyp	Ref	Expression
1		unitrrg.e	$⊢ E = RLReg (R)$
2		unitrrg.u	$⊢ U = Unit (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 2	unitcl	$⊢ x \in U \to x \in {Base}_{R}$
5	4	adantl	$⊢ (R \in Ring \land x \in U) \to x \in {Base}_{R}$
6		oveq2	$⊢ x \cdot_{R} y = 0_{R} \to {inv}_{r} (R) (x) \cdot_{R} (x \cdot_{R} y) = {inv}_{r} (R) (x) \cdot_{R} 0_{R}$
7		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	2 7 8 9	unitlinv	$⊢ (R \in Ring \land x \in U) \to {inv}_{r} (R) (x) \cdot_{R} x = 1_{R}$
11	10	adantr	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to {inv}_{r} (R) (x) \cdot_{R} x = 1_{R}$
12	11	oveq1d	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to ({inv}_{r} (R) (x) \cdot_{R} x) \cdot_{R} y = 1_{R} \cdot_{R} y$
13		simpll	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to R \in Ring$
14	2 7 3	ringinvcl	$⊢ (R \in Ring \land x \in U) \to {inv}_{r} (R) (x) \in {Base}_{R}$
15	14	adantr	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to {inv}_{r} (R) (x) \in {Base}_{R}$
16	5	adantr	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to x \in {Base}_{R}$
17		simpr	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to y \in {Base}_{R}$
18	3 8	ringass	$⊢ (R \in Ring \land ({inv}_{r} (R) (x) \in {Base}_{R} \land x \in {Base}_{R} \land y \in {Base}_{R})) \to ({inv}_{r} (R) (x) \cdot_{R} x) \cdot_{R} y = {inv}_{r} (R) (x) \cdot_{R} (x \cdot_{R} y)$
19	13 15 16 17 18	syl13anc	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to ({inv}_{r} (R) (x) \cdot_{R} x) \cdot_{R} y = {inv}_{r} (R) (x) \cdot_{R} (x \cdot_{R} y)$
20	3 8 9	ringlidm	$⊢ (R \in Ring \land y \in {Base}_{R}) \to 1_{R} \cdot_{R} y = y$
21	20	adantlr	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to 1_{R} \cdot_{R} y = y$
22	12 19 21	3eqtr3d	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to {inv}_{r} (R) (x) \cdot_{R} (x \cdot_{R} y) = y$
23		eqid	$⊢ 0_{R} = 0_{R}$
24	3 8 23	ringrz	$⊢ (R \in Ring \land {inv}_{r} (R) (x) \in {Base}_{R}) \to {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R}$
25	13 15 24	syl2anc	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R}$
26	22 25	eqeq12d	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to ({inv}_{r} (R) (x) \cdot_{R} (x \cdot_{R} y) = {inv}_{r} (R) (x) \cdot_{R} 0_{R} \leftrightarrow y = 0_{R})$
27	6 26	syl5ib	$⊢ ((R \in Ring \land x \in U) \land y \in {Base}_{R}) \to (x \cdot_{R} y = 0_{R} \to y = 0_{R})$
28	27	ralrimiva	$⊢ (R \in Ring \land x \in U) \to \forall y \in {Base}_{R} (x \cdot_{R} y = 0_{R} \to y = 0_{R})$
29	1 3 8 23	isrrg	$⊢ x \in E \leftrightarrow (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x \cdot_{R} y = 0_{R} \to y = 0_{R}))$
30	5 28 29	sylanbrc	$⊢ (R \in Ring \land x \in U) \to x \in E$
31	30	ex	$⊢ R \in Ring \to (x \in U \to x \in E)$
32	31	ssrdv	$⊢ R \in Ring \to U \subseteq E$

Metamath Proof Explorer

Theorem unitrrg

Proof