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