This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝐴 ∈ ( 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 ‘ 𝑅 ) → 𝑉 ⊆ 𝑈 )