# 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}={R}{↾}_{𝑠}{A}$
subrguss.2 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
subrguss.3 ${⊢}{V}=\mathrm{Unit}\left({S}\right)$
Assertion subrguss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\subseteq {U}$

### Proof

Step Hyp Ref Expression
1 subrguss.1 ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrguss.2 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
3 subrguss.3 ${⊢}{V}=\mathrm{Unit}\left({S}\right)$
4 simpr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}\in {V}$
5 eqid ${⊢}{1}_{{S}}={1}_{{S}}$
6 eqid ${⊢}{\parallel }_{r}\left({S}\right)={\parallel }_{r}\left({S}\right)$
7 eqid ${⊢}{opp}_{r}\left({S}\right)={opp}_{r}\left({S}\right)$
8 eqid ${⊢}{\parallel }_{r}\left({opp}_{r}\left({S}\right)\right)={\parallel }_{r}\left({opp}_{r}\left({S}\right)\right)$
9 3 5 6 7 8 isunit ${⊢}{x}\in {V}↔\left({x}{\parallel }_{r}\left({S}\right){1}_{{S}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({S}\right)\right){1}_{{S}}\right)$
10 4 9 sylib ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to \left({x}{\parallel }_{r}\left({S}\right){1}_{{S}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({S}\right)\right){1}_{{S}}\right)$
11 10 simpld ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\parallel }_{r}\left({S}\right){1}_{{S}}$
12 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
13 1 12 subrg1 ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}={1}_{{S}}$
14 13 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {1}_{{R}}={1}_{{S}}$
15 11 14 breqtrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\parallel }_{r}\left({S}\right){1}_{{R}}$
16 eqid ${⊢}{\parallel }_{r}\left({R}\right)={\parallel }_{r}\left({R}\right)$
17 1 16 6 subrgdvds ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\parallel }_{r}\left({S}\right)\subseteq {\parallel }_{r}\left({R}\right)$
18 17 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {\parallel }_{r}\left({S}\right)\subseteq {\parallel }_{r}\left({R}\right)$
19 18 ssbrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to \left({x}{\parallel }_{r}\left({S}\right){1}_{{R}}\to {x}{\parallel }_{r}\left({R}\right){1}_{{R}}\right)$
20 15 19 mpd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\parallel }_{r}\left({R}\right){1}_{{R}}$
21 1 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{{S}}$
22 21 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {A}={\mathrm{Base}}_{{S}}$
23 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
24 23 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
25 24 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
26 22 25 eqsstrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {\mathrm{Base}}_{{S}}\subseteq {\mathrm{Base}}_{{R}}$
27 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
28 27 3 unitcl ${⊢}{x}\in {V}\to {x}\in {\mathrm{Base}}_{{S}}$
29 28 adantl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}\in {\mathrm{Base}}_{{S}}$
30 26 29 sseldd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}\in {\mathrm{Base}}_{{R}}$
31 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
32 eqid ${⊢}{inv}_{r}\left({S}\right)={inv}_{r}\left({S}\right)$
33 3 32 27 ringinvcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {\mathrm{Base}}_{{S}}$
34 31 33 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {\mathrm{Base}}_{{S}}$
35 26 34 sseldd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {\mathrm{Base}}_{{R}}$
36 eqid ${⊢}{opp}_{r}\left({R}\right)={opp}_{r}\left({R}\right)$
37 36 23 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{opp}_{r}\left({R}\right)}$
38 eqid ${⊢}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)={\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)$
39 eqid ${⊢}{\cdot }_{{opp}_{r}\left({R}\right)}={\cdot }_{{opp}_{r}\left({R}\right)}$
40 37 38 39 dvdsrmul ${⊢}\left({x}\in {\mathrm{Base}}_{{R}}\wedge {inv}_{r}\left({S}\right)\left({x}\right)\in {\mathrm{Base}}_{{R}}\right)\to {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({inv}_{r}\left({S}\right)\left({x}\right){\cdot }_{{opp}_{r}\left({R}\right)}{x}\right)$
41 30 35 40 syl2anc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({inv}_{r}\left({S}\right)\left({x}\right){\cdot }_{{opp}_{r}\left({R}\right)}{x}\right)$
42 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
43 23 42 36 39 opprmul ${⊢}{inv}_{r}\left({S}\right)\left({x}\right){\cdot }_{{opp}_{r}\left({R}\right)}{x}={x}{\cdot }_{{R}}{inv}_{r}\left({S}\right)\left({x}\right)$
44 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
45 3 32 44 5 unitrinv ${⊢}\left({S}\in \mathrm{Ring}\wedge {x}\in {V}\right)\to {x}{\cdot }_{{S}}{inv}_{r}\left({S}\right)\left({x}\right)={1}_{{S}}$
46 31 45 sylan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\cdot }_{{S}}{inv}_{r}\left({S}\right)\left({x}\right)={1}_{{S}}$
47 1 42 ressmulr ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
48 47 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {\cdot }_{{R}}={\cdot }_{{S}}$
49 48 oveqd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\cdot }_{{R}}{inv}_{r}\left({S}\right)\left({x}\right)={x}{\cdot }_{{S}}{inv}_{r}\left({S}\right)\left({x}\right)$
50 46 49 14 3eqtr4d ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\cdot }_{{R}}{inv}_{r}\left({S}\right)\left({x}\right)={1}_{{R}}$
51 43 50 syl5eq ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {inv}_{r}\left({S}\right)\left({x}\right){\cdot }_{{opp}_{r}\left({R}\right)}{x}={1}_{{R}}$
52 41 51 breqtrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}$
53 2 12 16 36 38 isunit ${⊢}{x}\in {U}↔\left({x}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {x}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
54 20 52 53 sylanbrc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {V}\right)\to {x}\in {U}$
55 54 ex ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({x}\in {V}\to {x}\in {U}\right)$
56 55 ssrdv ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {V}\subseteq {U}$