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 โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
unitmulcl.2 โŠข ยท = ( .r โ€˜ ๐‘… )
unitmulclb.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
Assertion unitmulclb ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†” ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) ) )

Proof

Step Hyp Ref Expression
1 unitmulcl.1 โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
2 unitmulcl.2 โŠข ยท = ( .r โ€˜ ๐‘… )
3 unitmulclb.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
4 simp1 โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘… โˆˆ CRing )
5 simp2 โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ โˆˆ ๐ต )
6 simp3 โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ ๐ต )
7 eqid โŠข ( โˆฅr โ€˜ ๐‘… ) = ( โˆฅr โ€˜ ๐‘… )
8 3 7 2 dvdsrmul โŠข ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘Œ ยท ๐‘‹ ) )
9 5 6 8 syl2anc โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘Œ ยท ๐‘‹ ) )
10 3 2 crngcom โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) = ( ๐‘Œ ยท ๐‘‹ ) )
11 9 10 breqtrrd โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) )
12 1 7 dvdsunit โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) โˆง ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) โ†’ ๐‘‹ โˆˆ ๐‘ˆ )
13 12 3expia โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘‹ โˆˆ ๐‘ˆ ) )
14 4 11 13 syl2anc โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘‹ โˆˆ ๐‘ˆ ) )
15 3 7 2 dvdsrmul โŠข ( ( ๐‘Œ โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) )
16 6 5 15 syl2anc โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) )
17 1 7 dvdsunit โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) โˆง ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) โ†’ ๐‘Œ โˆˆ ๐‘ˆ )
18 17 3expia โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘Œ ( โˆฅr โ€˜ ๐‘… ) ( ๐‘‹ ยท ๐‘Œ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘Œ โˆˆ ๐‘ˆ ) )
19 4 16 18 syl2anc โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ๐‘Œ โˆˆ ๐‘ˆ ) )
20 14 19 jcad โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†’ ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) ) )
21 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
22 21 3ad2ant1 โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ๐‘… โˆˆ Ring )
23 1 2 unitmulcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ )
24 23 3expib โŠข ( ๐‘… โˆˆ Ring โ†’ ( ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) )
25 22 24 syl โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ ) )
26 20 25 impbid โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐‘ˆ โ†” ( ๐‘‹ โˆˆ ๐‘ˆ โˆง ๐‘Œ โˆˆ ๐‘ˆ ) ) )