Metamath Proof Explorer

Theorem subrginv

Description: A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses subrginv.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
subrginv.2 ⊢ 𝐼 = ( invr ‘ 𝑅 )
subrginv.3 ⊢ 𝑈 = ( Unit ‘ 𝑆 )
subrginv.4 ⊢ 𝐽 = ( invr ‘ 𝑆 )
Assertion subrginv ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) = ( 𝐽 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 subrginv.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrginv.2 ⊢ 𝐼 = ( invr ‘ 𝑅 )
3 subrginv.3 ⊢ 𝑈 = ( Unit ‘ 𝑆 )
4 subrginv.4 ⊢ 𝐽 = ( invr ‘ 𝑆 )
5 subrgrcl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
6 5 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ Ring )
7 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
10 7 9 eqsstrrd ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) )
11 10 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) )
12 1 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
13 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 3 4 13 ringinvcl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝐽 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
15 12 14 sylan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐽 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
16 11 15 sseldd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐽 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
17 13 3 unitcl ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑆 ) )
18 17 adantl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
19 11 18 sseldd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
20 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
21 1 20 3 subrguss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ⊆ ( Unit ‘ 𝑅 ) )
22 21 sselda ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Unit ‘ 𝑅 ) )
23 20 2 8 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
24 5 22 23 syl2an2r ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26 8 25 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐽 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) ) )
27 6 16 19 24 26 syl13anc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) ) )
28 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
29 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
30 3 4 28 29 unitlinv ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) = ( 1r ‘ 𝑆 ) )
31 12 30 sylan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) = ( 1r ‘ 𝑆 ) )
32 1 25 ressmulr ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
34 33 oveqd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑋 ) )
35 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
36 1 35 subrg1 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
37 36 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
38 31 34 37 3eqtr4d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
39 38 oveq1d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) )
40 20 2 25 35 unitrinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) )
41 5 22 40 syl2an2r ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) )
42 41 oveq2d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) ) = ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
43 27 39 42 3eqtr3d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
44 8 25 35 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
45 5 24 44 syl2an2r ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ 𝑋 ) )
46 8 25 35 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐽 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝐽 ‘ 𝑋 ) )
47 5 16 46 syl2an2r ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐽 ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝐽 ‘ 𝑋 ) )
48 43 45 47 3eqtr3d ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) = ( 𝐽 ‘ 𝑋 ) )