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 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 ‘ 𝑅 ) → 𝑉 ⊆ 𝑈 )