Metamath Proof Explorer

Theorem unitmulcl

Description: The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses unitmulcl.1 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
unitmulcl.2
Assertion unitmulcl

Proof

Step Hyp Ref Expression
1 unitmulcl.1 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
2 unitmulcl.2
3 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {R}\in \mathrm{Ring}$
4 simp3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {Y}\in {U}$
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 5 1 unitcl ${⊢}{Y}\in {U}\to {Y}\in {\mathrm{Base}}_{{R}}$
7 4 6 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {Y}\in {\mathrm{Base}}_{{R}}$
8 simp2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {X}\in {U}$
9 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
10 eqid ${⊢}{\parallel }_{r}\left({R}\right)={\parallel }_{r}\left({R}\right)$
11 eqid ${⊢}{opp}_{r}\left({R}\right)={opp}_{r}\left({R}\right)$
12 eqid ${⊢}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)={\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)$
13 1 9 10 11 12 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)$
14 8 13 sylib ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to \left({X}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {X}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
15 14 simpld ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {X}{\parallel }_{r}\left({R}\right){1}_{{R}}$
16 5 10 2 dvdsrmul1
17 3 7 15 16 syl3anc
18 5 2 9 ringlidm
19 3 7 18 syl2anc
20 17 19 breqtrd
21 1 9 10 11 12 isunit ${⊢}{Y}\in {U}↔\left({Y}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {Y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
22 4 21 sylib ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to \left({Y}{\parallel }_{r}\left({R}\right){1}_{{R}}\wedge {Y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)$
23 22 simpld ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {Y}{\parallel }_{r}\left({R}\right){1}_{{R}}$
24 5 10 dvdsrtr
25 3 20 23 24 syl3anc
26 11 opprring ${⊢}{R}\in \mathrm{Ring}\to {opp}_{r}\left({R}\right)\in \mathrm{Ring}$
27 3 26 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {opp}_{r}\left({R}\right)\in \mathrm{Ring}$
28 eqid ${⊢}{\cdot }_{{opp}_{r}\left({R}\right)}={\cdot }_{{opp}_{r}\left({R}\right)}$
29 5 2 11 28 opprmul
30 5 1 unitcl ${⊢}{X}\in {U}\to {X}\in {\mathrm{Base}}_{{R}}$
31 8 30 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {X}\in {\mathrm{Base}}_{{R}}$
32 22 simprd ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {Y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}$
33 11 5 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{opp}_{r}\left({R}\right)}$
34 33 12 28 dvdsrmul1 ${⊢}\left({opp}_{r}\left({R}\right)\in \mathrm{Ring}\wedge {X}\in {\mathrm{Base}}_{{R}}\wedge {Y}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}\right)\to \left({Y}{\cdot }_{{opp}_{r}\left({R}\right)}{X}\right){\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({1}_{{R}}{\cdot }_{{opp}_{r}\left({R}\right)}{X}\right)$
35 27 31 32 34 syl3anc ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to \left({Y}{\cdot }_{{opp}_{r}\left({R}\right)}{X}\right){\parallel }_{r}\left({opp}_{r}\left({R}\right)\right)\left({1}_{{R}}{\cdot }_{{opp}_{r}\left({R}\right)}{X}\right)$
36 5 2 11 28 opprmul
37 5 2 9 ringridm
38 3 31 37 syl2anc
39 36 38 syl5eq ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {1}_{{R}}{\cdot }_{{opp}_{r}\left({R}\right)}{X}={X}$
40 35 39 breqtrd ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to \left({Y}{\cdot }_{{opp}_{r}\left({R}\right)}{X}\right){\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){X}$
41 29 40 eqbrtrrid
42 14 simprd ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {U}\wedge {Y}\in {U}\right)\to {X}{\parallel }_{r}\left({opp}_{r}\left({R}\right)\right){1}_{{R}}$
43 33 12 dvdsrtr
44 27 41 42 43 syl3anc
45 1 9 10 11 12 isunit
46 25 44 45 sylanbrc