Metamath Proof Explorer

Theorem unitpropd

Description: The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses rngidpropd.1 
|- ( ph -> B = ( Base ` K ) )
rngidpropd.2 
|- ( ph -> B = ( Base ` L ) )
rngidpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion unitpropd 
|- ( ph -> ( Unit ` K ) = ( Unit ` L ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 rngidpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 rngidpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
4 1 2 3 rngidpropd 
 |-  ( ph -> ( 1r ` K ) = ( 1r ` L ) )
5 4 breq2d 
 |-  ( ph -> ( z ( ||r ` K ) ( 1r ` K ) <-> z ( ||r ` K ) ( 1r ` L ) ) )
6 4 breq2d 
 |-  ( ph -> ( z ( ||r ` ( oppR ` K ) ) ( 1r ` K ) <-> z ( ||r ` ( oppR ` K ) ) ( 1r ` L ) ) )
7 5 6 anbi12d 
 |-  ( ph -> ( ( z ( ||r ` K ) ( 1r ` K ) /\ z ( ||r ` ( oppR ` K ) ) ( 1r ` K ) ) <-> ( z ( ||r ` K ) ( 1r ` L ) /\ z ( ||r ` ( oppR ` K ) ) ( 1r ` L ) ) ) )
8 1 2 3 dvdsrpropd 
 |-  ( ph -> ( ||r ` K ) = ( ||r ` L ) )
9 8 breqd 
 |-  ( ph -> ( z ( ||r ` K ) ( 1r ` L ) <-> z ( ||r ` L ) ( 1r ` L ) ) )
10 eqid 
 |-  ( oppR ` K ) = ( oppR ` K )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 10 11 opprbas 
 |-  ( Base ` K ) = ( Base ` ( oppR ` K ) )
13 1 12 eqtrdi 
 |-  ( ph -> B = ( Base ` ( oppR ` K ) ) )
14 eqid 
 |-  ( oppR ` L ) = ( oppR ` L )
15 eqid 
 |-  ( Base ` L ) = ( Base ` L )
16 14 15 opprbas 
 |-  ( Base ` L ) = ( Base ` ( oppR ` L ) )
17 2 16 eqtrdi 
 |-  ( ph -> B = ( Base ` ( oppR ` L ) ) )
18 3 ancom2s 
 |-  ( ( ph /\ ( y e. B /\ x e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
19 eqid 
 |-  ( .r ` K ) = ( .r ` K )
20 eqid 
 |-  ( .r ` ( oppR ` K ) ) = ( .r ` ( oppR ` K ) )
21 11 19 10 20 opprmul 
 |-  ( y ( .r ` ( oppR ` K ) ) x ) = ( x ( .r ` K ) y )
22 eqid 
 |-  ( .r ` L ) = ( .r ` L )
23 eqid 
 |-  ( .r ` ( oppR ` L ) ) = ( .r ` ( oppR ` L ) )
24 15 22 14 23 opprmul 
 |-  ( y ( .r ` ( oppR ` L ) ) x ) = ( x ( .r ` L ) y )
25 18 21 24 3eqtr4g 
 |-  ( ( ph /\ ( y e. B /\ x e. B ) ) -> ( y ( .r ` ( oppR ` K ) ) x ) = ( y ( .r ` ( oppR ` L ) ) x ) )
26 13 17 25 dvdsrpropd 
 |-  ( ph -> ( ||r ` ( oppR ` K ) ) = ( ||r ` ( oppR ` L ) ) )
27 26 breqd 
 |-  ( ph -> ( z ( ||r ` ( oppR ` K ) ) ( 1r ` L ) <-> z ( ||r ` ( oppR ` L ) ) ( 1r ` L ) ) )
28 9 27 anbi12d 
 |-  ( ph -> ( ( z ( ||r ` K ) ( 1r ` L ) /\ z ( ||r ` ( oppR ` K ) ) ( 1r ` L ) ) <-> ( z ( ||r ` L ) ( 1r ` L ) /\ z ( ||r ` ( oppR ` L ) ) ( 1r ` L ) ) ) )
29 7 28 bitrd 
 |-  ( ph -> ( ( z ( ||r ` K ) ( 1r ` K ) /\ z ( ||r ` ( oppR ` K ) ) ( 1r ` K ) ) <-> ( z ( ||r ` L ) ( 1r ` L ) /\ z ( ||r ` ( oppR ` L ) ) ( 1r ` L ) ) ) )
30 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
31 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
32 eqid 
 |-  ( ||r ` K ) = ( ||r ` K )
33 eqid 
 |-  ( ||r ` ( oppR ` K ) ) = ( ||r ` ( oppR ` K ) )
34 30 31 32 10 33 isunit 
 |-  ( z e. ( Unit ` K ) <-> ( z ( ||r ` K ) ( 1r ` K ) /\ z ( ||r ` ( oppR ` K ) ) ( 1r ` K ) ) )
35 eqid 
 |-  ( Unit ` L ) = ( Unit ` L )
36 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
37 eqid 
 |-  ( ||r ` L ) = ( ||r ` L )
38 eqid 
 |-  ( ||r ` ( oppR ` L ) ) = ( ||r ` ( oppR ` L ) )
39 35 36 37 14 38 isunit 
 |-  ( z e. ( Unit ` L ) <-> ( z ( ||r ` L ) ( 1r ` L ) /\ z ( ||r ` ( oppR ` L ) ) ( 1r ` L ) ) )
40 29 34 39 3bitr4g 
 |-  ( ph -> ( z e. ( Unit ` K ) <-> z e. ( Unit ` L ) ) )
41 40 eqrdv 
 |-  ( ph -> ( Unit ` K ) = ( Unit ` L ) )