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 φ B = Base K
rngidpropd.2 φ B = Base L
rngidpropd.3 φ x B y B x K y = x L y
Assertion unitpropd φ Unit K = Unit L

Proof

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