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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝐴 ∈ ( 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 ‘ 𝑅 ) → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐴 ) ) )