Theorem unitrrg

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

	Ref	Expression
Hypotheses	unitrrg.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	unitrrg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	unitrrg	⊢ ( 𝑅 ∈ Ring → 𝑈 ⊆ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		unitrrg.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2		unitrrg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 2	unitcl	⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑅 ) )
5	4	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
6		oveq2	⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
7		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10	2 7 8 9	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
11	10	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
12	11	oveq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) )
13		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
14	2 7 3	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
15	14	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
16	5	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
17		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
18	3 8	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
19	13 15 16 17 18	syl13anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
20	3 8 9	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
21	20	adantlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
22	12 19 21	3eqtr3d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = 𝑦 )
23		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24	3 8 23	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
25	13 15 24	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
26	22 25	eqeq12d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ↔ 𝑦 = ( 0g ‘ 𝑅 ) ) )
27	6 26	imbitrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) )
28	27	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) )
29	1 3 8 23	isrrg	⊢ ( 𝑥 ∈ 𝐸 ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
30	5 28 29	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐸 )
31	30	ex	⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐸 ) )
32	31	ssrdv	⊢ ( 𝑅 ∈ Ring → 𝑈 ⊆ 𝐸 )