This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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