Theorem subrgunit

Description: An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrgugrp.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
	subrgugrp.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	subrgugrp.3	⊢ 𝑉 = ( Unit ‘ 𝑆 )
	subrgunit.4	⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion	subrgunit	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		subrgugrp.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		subrgugrp.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		subrgugrp.3	⊢ 𝑉 = ( Unit ‘ 𝑆 )
4		subrgunit.4	⊢ 𝐼 = ( invr ‘ 𝑅 )
5	1 2 3	subrguss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ⊆ 𝑈 )
6	5	sselda	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑈 )
7		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8	7 3	unitcl	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( Base ‘ 𝑆 ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
10	1	subrgbas	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐴 = ( Base ‘ 𝑆 ) )
12	9 11	eleqtrrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐴 )
13	1	subrgring	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
14		eqid	⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
15	3 14 7	ringinvcl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑉 ) → ( ( invr ‘ 𝑆 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
16	13 15	sylan	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( invr ‘ 𝑆 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
17	1 4 3 14	subrginv	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ 𝑋 ) = ( ( invr ‘ 𝑆 ) ‘ 𝑋 ) )
18	16 17 11	3eltr4d	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 )
19	6 12 18	3jca	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) )
20		simpr2	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ∈ 𝐴 )
21	10	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
22	20 21	eleqtrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
23		simpr3	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 )
24	23 21	eleqtrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
25		eqid	⊢ ( ∥r ‘ 𝑆 ) = ( ∥r ‘ 𝑆 )
26		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
27	7 25 26	dvdsrmul	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → 𝑋 ( ∥r ‘ 𝑆 ) ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) )
28	22 24 27	syl2anc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ( ∥r ‘ 𝑆 ) ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) )
29		subrgrcl	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
30	29	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑅 ∈ Ring )
31		simpr1	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ∈ 𝑈 )
32		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
34	2 4 32 33	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
35	30 31 34	syl2anc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
36	1 32	ressmulr	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
37	36	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
38	37	oveqd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) )
39	1 33	subrg1	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
40	39	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
41	35 38 40	3eqtr3d	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) = ( 1r ‘ 𝑆 ) )
42	28 41	breqtrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) )
43		eqid	⊢ ( oppr ‘ 𝑆 ) = ( oppr ‘ 𝑆 )
44	43 7	opprbas	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( oppr ‘ 𝑆 ) )
45		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑆 ) ) = ( ∥r ‘ ( oppr ‘ 𝑆 ) )
46		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑆 ) ) = ( .r ‘ ( oppr ‘ 𝑆 ) )
47	44 45 46	dvdsrmul	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑋 ) )
48	22 24 47	syl2anc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑋 ) )
49	7 26 43 46	opprmul	⊢ ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑋 ) = ( 𝑋 ( .r ‘ 𝑆 ) ( 𝐼 ‘ 𝑋 ) )
50	2 4 32 33	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) )
51	30 31 50	syl2anc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) )
52	37	oveqd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝑋 ( .r ‘ 𝑆 ) ( 𝐼 ‘ 𝑋 ) ) )
53	51 52 40	3eqtr3d	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝑆 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝑆 ) )
54	49 53	syl5eq	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → ( ( 𝐼 ‘ 𝑋 ) ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑋 ) = ( 1r ‘ 𝑆 ) )
55	48 54	breqtrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑆 ) )
56		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
57	3 56 25 43 45	isunit	⊢ ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑆 ) ) )
58	42 55 57	sylanbrc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) → 𝑋 ∈ 𝑉 )
59	19 58	impbida	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) )