Theorem subrguss

Description: A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	subrguss.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
	subrguss.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	subrguss.3	⊢ 𝑉 = ( Unit ‘ 𝑆 )
Assertion	subrguss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		subrguss.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		subrguss.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		subrguss.3	⊢ 𝑉 = ( Unit ‘ 𝑆 )
4		simpr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
5		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
6		eqid	⊢ ( ∥r ‘ 𝑆 ) = ( ∥r ‘ 𝑆 )
7		eqid	⊢ ( oppr ‘ 𝑆 ) = ( oppr ‘ 𝑆 )
8		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑆 ) ) = ( ∥r ‘ ( oppr ‘ 𝑆 ) )
9	3 5 6 7 8	isunit	⊢ ( 𝑥 ∈ 𝑉 ↔ ( 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑆 ) ) )
10	4 9	sylib	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑆 ) ) )
11	10	simpld	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) )
12		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
13	1 12	subrg1	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
14	13	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
15	11 14	breqtrrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) )
16		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
17	1 16 6	subrgdvds	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ∥r ‘ 𝑆 ) ⊆ ( ∥r ‘ 𝑅 ) )
18	17	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∥r ‘ 𝑆 ) ⊆ ( ∥r ‘ 𝑅 ) )
19	18	ssbrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) → 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
20	15 19	mpd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
21	1	subrgbas	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
22	21	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝐴 = ( Base ‘ 𝑆 ) )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24	23	subrgss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
25	24	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
26	22 25	eqsstrrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) )
27		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
28	27 3	unitcl	⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑆 ) )
29	28	adantl	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
30	26 29	sseldd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
31	1	subrgring	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
32		eqid	⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
33	3 32 27	ringinvcl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑥 ∈ 𝑉 ) → ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
34	31 33	sylan	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
35	26 34	sseldd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
36		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
37	36 23	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
38		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
39		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
40	37 38 39	dvdsrmul	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
41	30 35 40	syl2anc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
42		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
43	23 42 36 39	opprmul	⊢ ( ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) )
44		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
45	3 32 44 5	unitrinv	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 1r ‘ 𝑆 ) )
46	31 45	sylan	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 1r ‘ 𝑆 ) )
47	1 42	ressmulr	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
48	47	adantr	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
49	48	oveqd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 𝑥 ( .r ‘ 𝑆 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ) )
50	46 49 14	3eqtr4d	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 1r ‘ 𝑅 ) )
51	43 50	syl5eq	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
52	41 51	breqtrd	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
53	2 12 16 36 38	isunit	⊢ ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
54	20 52 53	sylanbrc	⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑈 )
55	54	ex	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑈 ) )
56	55	ssrdv	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑉 ⊆ 𝑈 )