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