Metamath Proof Explorer

Theorem unitmulclb

Description: Reversal of unitmulcl in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses unitmulcl.1 
|- U = ( Unit ` R )
unitmulcl.2 
|- .x. = ( .r ` R )
unitmulclb.1 
|- B = ( Base ` R )
Assertion unitmulclb 
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U <-> ( X e. U /\ Y e. U ) ) )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 
 |-  U = ( Unit ` R )
2 unitmulcl.2 
 |-  .x. = ( .r ` R )
3 unitmulclb.1 
 |-  B = ( Base ` R )
4 simp1 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> R e. CRing )
5 simp2 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> X e. B )
6 simp3 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> Y e. B )
7 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
8 3 7 2 dvdsrmul 
 |-  ( ( X e. B /\ Y e. B ) -> X ( ||r ` R ) ( Y .x. X ) )
9 5 6 8 syl2anc 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> X ( ||r ` R ) ( Y .x. X ) )
10 3 2 crngcom 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
11 9 10 breqtrrd 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> X ( ||r ` R ) ( X .x. Y ) )
12 1 7 dvdsunit 
 |-  ( ( R e. CRing /\ X ( ||r ` R ) ( X .x. Y ) /\ ( X .x. Y ) e. U ) -> X e. U )
13 12 3expia 
 |-  ( ( R e. CRing /\ X ( ||r ` R ) ( X .x. Y ) ) -> ( ( X .x. Y ) e. U -> X e. U ) )
14 4 11 13 syl2anc 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U -> X e. U ) )
15 3 7 2 dvdsrmul 
 |-  ( ( Y e. B /\ X e. B ) -> Y ( ||r ` R ) ( X .x. Y ) )
16 6 5 15 syl2anc 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> Y ( ||r ` R ) ( X .x. Y ) )
17 1 7 dvdsunit 
 |-  ( ( R e. CRing /\ Y ( ||r ` R ) ( X .x. Y ) /\ ( X .x. Y ) e. U ) -> Y e. U )
18 17 3expia 
 |-  ( ( R e. CRing /\ Y ( ||r ` R ) ( X .x. Y ) ) -> ( ( X .x. Y ) e. U -> Y e. U ) )
19 4 16 18 syl2anc 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U -> Y e. U ) )
20 14 19 jcad 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U -> ( X e. U /\ Y e. U ) ) )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 21 3ad2ant1 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> R e. Ring )
23 1 2 unitmulcl 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )
24 23 3expib 
 |-  ( R e. Ring -> ( ( X e. U /\ Y e. U ) -> ( X .x. Y ) e. U ) )
25 22 24 syl 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X e. U /\ Y e. U ) -> ( X .x. Y ) e. U ) )
26 20 25 impbid 
 |-  ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U <-> ( X e. U /\ Y e. U ) ) )