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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion unitpropd ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 rngidpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 rngidpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
4 1 2 3 rngidpropd ( 𝜑 → ( 1r𝐾 ) = ( 1r𝐿 ) )
5 4 breq2d ( 𝜑 → ( 𝑧 ( ∥r𝐾 ) ( 1r𝐾 ) ↔ 𝑧 ( ∥r𝐾 ) ( 1r𝐿 ) ) )
6 4 breq2d ( 𝜑 → ( 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐾 ) ↔ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐿 ) ) )
7 5 6 anbi12d ( 𝜑 → ( ( 𝑧 ( ∥r𝐾 ) ( 1r𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐾 ) ) ↔ ( 𝑧 ( ∥r𝐾 ) ( 1r𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐿 ) ) ) )
8 1 2 3 dvdsrpropd ( 𝜑 → ( ∥r𝐾 ) = ( ∥r𝐿 ) )
9 8 breqd ( 𝜑 → ( 𝑧 ( ∥r𝐾 ) ( 1r𝐿 ) ↔ 𝑧 ( ∥r𝐿 ) ( 1r𝐿 ) ) )
10 eqid ( oppr𝐾 ) = ( oppr𝐾 )
11 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 10 11 opprbas ( Base ‘ 𝐾 ) = ( Base ‘ ( oppr𝐾 ) )
13 1 12 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( oppr𝐾 ) ) )
14 eqid ( oppr𝐿 ) = ( oppr𝐿 )
15 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
16 14 15 opprbas ( Base ‘ 𝐿 ) = ( Base ‘ ( oppr𝐿 ) )
17 2 16 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( oppr𝐿 ) ) )
18 3 ancom2s ( ( 𝜑 ∧ ( 𝑦𝐵𝑥𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
19 eqid ( .r𝐾 ) = ( .r𝐾 )
20 eqid ( .r ‘ ( oppr𝐾 ) ) = ( .r ‘ ( oppr𝐾 ) )
21 11 19 10 20 opprmul ( 𝑦 ( .r ‘ ( oppr𝐾 ) ) 𝑥 ) = ( 𝑥 ( .r𝐾 ) 𝑦 )
22 eqid ( .r𝐿 ) = ( .r𝐿 )
23 eqid ( .r ‘ ( oppr𝐿 ) ) = ( .r ‘ ( oppr𝐿 ) )
24 15 22 14 23 opprmul ( 𝑦 ( .r ‘ ( oppr𝐿 ) ) 𝑥 ) = ( 𝑥 ( .r𝐿 ) 𝑦 )
25 18 21 24 3eqtr4g ( ( 𝜑 ∧ ( 𝑦𝐵𝑥𝐵 ) ) → ( 𝑦 ( .r ‘ ( oppr𝐾 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr𝐿 ) ) 𝑥 ) )
26 13 17 25 dvdsrpropd ( 𝜑 → ( ∥r ‘ ( oppr𝐾 ) ) = ( ∥r ‘ ( oppr𝐿 ) ) )
27 26 breqd ( 𝜑 → ( 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐿 ) ↔ 𝑧 ( ∥r ‘ ( oppr𝐿 ) ) ( 1r𝐿 ) ) )
28 9 27 anbi12d ( 𝜑 → ( ( 𝑧 ( ∥r𝐾 ) ( 1r𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐿 ) ) ↔ ( 𝑧 ( ∥r𝐿 ) ( 1r𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐿 ) ) ( 1r𝐿 ) ) ) )
29 7 28 bitrd ( 𝜑 → ( ( 𝑧 ( ∥r𝐾 ) ( 1r𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐾 ) ) ↔ ( 𝑧 ( ∥r𝐿 ) ( 1r𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐿 ) ) ( 1r𝐿 ) ) ) )
30 eqid ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐾 )
31 eqid ( 1r𝐾 ) = ( 1r𝐾 )
32 eqid ( ∥r𝐾 ) = ( ∥r𝐾 )
33 eqid ( ∥r ‘ ( oppr𝐾 ) ) = ( ∥r ‘ ( oppr𝐾 ) )
34 30 31 32 10 33 isunit ( 𝑧 ∈ ( Unit ‘ 𝐾 ) ↔ ( 𝑧 ( ∥r𝐾 ) ( 1r𝐾 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐾 ) ) ( 1r𝐾 ) ) )
35 eqid ( Unit ‘ 𝐿 ) = ( Unit ‘ 𝐿 )
36 eqid ( 1r𝐿 ) = ( 1r𝐿 )
37 eqid ( ∥r𝐿 ) = ( ∥r𝐿 )
38 eqid ( ∥r ‘ ( oppr𝐿 ) ) = ( ∥r ‘ ( oppr𝐿 ) )
39 35 36 37 14 38 isunit ( 𝑧 ∈ ( Unit ‘ 𝐿 ) ↔ ( 𝑧 ( ∥r𝐿 ) ( 1r𝐿 ) ∧ 𝑧 ( ∥r ‘ ( oppr𝐿 ) ) ( 1r𝐿 ) ) )
40 29 34 39 3bitr4g ( 𝜑 → ( 𝑧 ∈ ( Unit ‘ 𝐾 ) ↔ 𝑧 ∈ ( Unit ‘ 𝐿 ) ) )
41 40 eqrdv ( 𝜑 → ( Unit ‘ 𝐾 ) = ( Unit ‘ 𝐿 ) )