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

Metamath Proof Explorer

Theorem oppr1

Description: Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
oppr1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion oppr1 1 = ( 1r ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 oppr1.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
6 3 4 1 5 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
7 6 eqeq1i ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 )
8 3 4 1 5 opprmul ⊢ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 )
9 8 eqeq1i ⊢ ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 )
10 7 9 anbi12ci ⊢ ( ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
11 10 ralbii ⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
12 11 anbi2i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
13 12 iotabii ⊢ ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
14 eqid ⊢ ( mulGrp ‘ 𝑂 ) = ( mulGrp ‘ 𝑂 )
15 1 3 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
16 14 15 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑂 ) )
17 14 5 mgpplusg ⊢ ( .r ‘ 𝑂 ) = ( +g ‘ ( mulGrp ‘ 𝑂 ) )
18 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑂 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑂 ) )
19 16 17 18 grpidval ⊢ ( 0g ‘ ( mulGrp ‘ 𝑂 ) ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) )
20 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
21 20 3 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
22 20 4 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
23 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
24 21 22 23 grpidval ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
25 13 19 24 3eqtr4i ⊢ ( 0g ‘ ( mulGrp ‘ 𝑂 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
26 eqid ⊢ ( 1r ‘ 𝑂 ) = ( 1r ‘ 𝑂 )
27 14 26 ringidval ⊢ ( 1r ‘ 𝑂 ) = ( 0g ‘ ( mulGrp ‘ 𝑂 ) )
28 20 2 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
29 25 27 28 3eqtr4ri ⊢ 1 = ( 1r ‘ 𝑂 )