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 = ( Unit ` R )
unitmulcl.2 
|- .x. = ( .r ` R )
Assertion unitmulcl 
|- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 
 |-  U = ( Unit ` R )
2 unitmulcl.2 
 |-  .x. = ( .r ` R )
3 simp1 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> R e. Ring )
4 simp3 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> Y e. U )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 1 unitcl 
 |-  ( Y e. U -> Y e. ( Base ` R ) )
7 4 6 syl 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> Y e. ( Base ` R ) )
8 simp2 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> X e. U )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
11 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
12 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
13 1 9 10 11 12 isunit 
 |-  ( X e. U <-> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
14 8 13 sylib 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
15 14 simpld 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> X ( ||r ` R ) ( 1r ` R ) )
16 5 10 2 dvdsrmul1 
 |-  ( ( R e. Ring /\ Y e. ( Base ` R ) /\ X ( ||r ` R ) ( 1r ` R ) ) -> ( X .x. Y ) ( ||r ` R ) ( ( 1r ` R ) .x. Y ) )
17 3 7 15 16 syl3anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) ( ||r ` R ) ( ( 1r ` R ) .x. Y ) )
18 5 2 9 ringlidm 
 |-  ( ( R e. Ring /\ Y e. ( Base ` R ) ) -> ( ( 1r ` R ) .x. Y ) = Y )
19 3 7 18 syl2anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( ( 1r ` R ) .x. Y ) = Y )
20 17 19 breqtrd 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) ( ||r ` R ) Y )
21 1 9 10 11 12 isunit 
 |-  ( Y e. U <-> ( Y ( ||r ` R ) ( 1r ` R ) /\ Y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
22 4 21 sylib 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( Y ( ||r ` R ) ( 1r ` R ) /\ Y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
23 22 simpld 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> Y ( ||r ` R ) ( 1r ` R ) )
24 5 10 dvdsrtr 
 |-  ( ( R e. Ring /\ ( X .x. Y ) ( ||r ` R ) Y /\ Y ( ||r ` R ) ( 1r ` R ) ) -> ( X .x. Y ) ( ||r ` R ) ( 1r ` R ) )
25 3 20 23 24 syl3anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) ( ||r ` R ) ( 1r ` R ) )
26 11 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
27 3 26 syl 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( oppR ` R ) e. Ring )
28 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
29 5 2 11 28 opprmul 
 |-  ( Y ( .r ` ( oppR ` R ) ) X ) = ( X .x. Y )
30 5 1 unitcl 
 |-  ( X e. U -> X e. ( Base ` R ) )
31 8 30 syl 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> X e. ( Base ` R ) )
32 22 simprd 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> Y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
33 11 5 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
34 33 12 28 dvdsrmul1 
 |-  ( ( ( oppR ` R ) e. Ring /\ X e. ( Base ` R ) /\ Y ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> ( Y ( .r ` ( oppR ` R ) ) X ) ( ||r ` ( oppR ` R ) ) ( ( 1r ` R ) ( .r ` ( oppR ` R ) ) X ) )
35 27 31 32 34 syl3anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( Y ( .r ` ( oppR ` R ) ) X ) ( ||r ` ( oppR ` R ) ) ( ( 1r ` R ) ( .r ` ( oppR ` R ) ) X ) )
36 5 2 11 28 opprmul 
 |-  ( ( 1r ` R ) ( .r ` ( oppR ` R ) ) X ) = ( X .x. ( 1r ` R ) )
37 5 2 9 ringridm 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> ( X .x. ( 1r ` R ) ) = X )
38 3 31 37 syl2anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. ( 1r ` R ) ) = X )
39 36 38 eqtrid 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( ( 1r ` R ) ( .r ` ( oppR ` R ) ) X ) = X )
40 35 39 breqtrd 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( Y ( .r ` ( oppR ` R ) ) X ) ( ||r ` ( oppR ` R ) ) X )
41 29 40 eqbrtrrid 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) ( ||r ` ( oppR ` R ) ) X )
42 14 simprd 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
43 33 12 dvdsrtr 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( X .x. Y ) ( ||r ` ( oppR ` R ) ) X /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> ( X .x. Y ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
44 27 41 42 43 syl3anc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
45 1 9 10 11 12 isunit 
 |-  ( ( X .x. Y ) e. U <-> ( ( X .x. Y ) ( ||r ` R ) ( 1r ` R ) /\ ( X .x. Y ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
46 25 44 45 sylanbrc 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )