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 ) )