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

Metamath Proof Explorer

Theorem opprunit

Description: Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses opprunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
opprunit.2 ⊢ 𝑆 = ( oppr ‘ 𝑅 )
Assertion opprunit 𝑈 = ( Unit ‘ 𝑆 )

Proof

Step Hyp Ref Expression
1 opprunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 opprunit.2 ⊢ 𝑆 = ( oppr ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 2 3 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 )
5 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
6 eqid ⊢ ( oppr ‘ 𝑆 ) = ( oppr ‘ 𝑆 )
7 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑆 ) ) = ( .r ‘ ( oppr ‘ 𝑆 ) )
8 4 5 6 7 opprmul ⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 3 9 2 5 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
11 8 10 eqtr2i ⊢ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 )
12 11 eqeq1i ⊢ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ↔ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
13 12 rexbii ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
14 13 anbi2i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
15 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
16 3 15 9 dvdsr ⊢ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
17 6 4 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑆 ) )
18 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑆 ) ) = ( ∥r ‘ ( oppr ‘ 𝑆 ) )
19 17 18 7 dvdsr ⊢ ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑆 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
20 14 16 19 3bitr4i ⊢ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑅 ) )
21 20 anbi2ci ⊢ ( ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) ↔ ( 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑅 ) ) )
22 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
23 eqid ⊢ ( ∥r ‘ 𝑆 ) = ( ∥r ‘ 𝑆 )
24 1 22 15 2 23 isunit ⊢ ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ) )
25 eqid ⊢ ( Unit ‘ 𝑆 ) = ( Unit ‘ 𝑆 )
26 2 22 oppr1 ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 )
27 25 26 23 6 18 isunit ⊢ ( 𝑥 ∈ ( Unit ‘ 𝑆 ) ↔ ( 𝑥 ( ∥r ‘ 𝑆 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑆 ) ) ( 1r ‘ 𝑅 ) ) )
28 21 24 27 3bitr4i ⊢ ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ( Unit ‘ 𝑆 ) )
29 28 eqriv ⊢ 𝑈 = ( Unit ‘ 𝑆 )