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	$⊢ U = Unit (R)$
	opprunit.2	$⊢ S = {opp}_{r} (R)$
Assertion	opprunit	$⊢ U = Unit (S)$

Proof

Step	Hyp	Ref	Expression
1		opprunit.1	$⊢ U = Unit (R)$
2		opprunit.2	$⊢ S = {opp}_{r} (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	2 3	opprbas	$⊢ {Base}_{R} = {Base}_{S}$
5		eqid	$⊢ \cdot_{S} = \cdot_{S}$
6		eqid	$⊢ {opp}_{r} (S) = {opp}_{r} (S)$
7		eqid	$⊢ \cdot_{{opp}_{r} (S)} = \cdot_{{opp}_{r} (S)}$
8	4 5 6 7	opprmul	$⊢ y \cdot_{{opp}_{r} (S)} x = x \cdot_{S} y$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10	3 9 2 5	opprmul	$⊢ x \cdot_{S} y = y \cdot_{R} x$
11	8 10	eqtr2i	$⊢ y \cdot_{R} x = y \cdot_{{opp}_{r} (S)} x$
12	11	eqeq1i	$⊢ y \cdot_{R} x = 1_{R} \leftrightarrow y \cdot_{{opp}_{r} (S)} x = 1_{R}$
13	12	rexbii	$⊢ \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R} \leftrightarrow \exists y \in {Base}_{R} y \cdot_{{opp}_{r} (S)} x = 1_{R}$
14	13	anbi2i	$⊢ (x \in {Base}_{R} \land \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R}) \leftrightarrow (x \in {Base}_{R} \land \exists y \in {Base}_{R} y \cdot_{{opp}_{r} (S)} x = 1_{R})$
15		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
16	3 15 9	dvdsr	$⊢ x ∥_{r} (R) 1_{R} \leftrightarrow (x \in {Base}_{R} \land \exists y \in {Base}_{R} y \cdot_{R} x = 1_{R})$
17	6 4	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (S)}$
18		eqid	$⊢ ∥_{r} ({opp}_{r} (S)) = ∥_{r} ({opp}_{r} (S))$
19	17 18 7	dvdsr	$⊢ x ∥_{r} ({opp}_{r} (S)) 1_{R} \leftrightarrow (x \in {Base}_{R} \land \exists y \in {Base}_{R} y \cdot_{{opp}_{r} (S)} x = 1_{R})$
20	14 16 19	3bitr4i	$⊢ x ∥_{r} (R) 1_{R} \leftrightarrow x ∥_{r} ({opp}_{r} (S)) 1_{R}$
21	20	anbi2ci	$⊢ (x ∥_{r} (R) 1_{R} \land x ∥_{r} (S) 1_{R}) \leftrightarrow (x ∥_{r} (S) 1_{R} \land x ∥_{r} ({opp}_{r} (S)) 1_{R})$
22		eqid	$⊢ 1_{R} = 1_{R}$
23		eqid	$⊢ ∥_{r} (S) = ∥_{r} (S)$
24	1 22 15 2 23	isunit	$⊢ x \in U \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} (S) 1_{R})$
25		eqid	$⊢ Unit (S) = Unit (S)$
26	2 22	oppr1	$⊢ 1_{R} = 1_{S}$
27	25 26 23 6 18	isunit	$⊢ x \in Unit (S) \leftrightarrow (x ∥_{r} (S) 1_{R} \land x ∥_{r} ({opp}_{r} (S)) 1_{R})$
28	21 24 27	3bitr4i	$⊢ x \in U \leftrightarrow x \in Unit (S)$
29	28	eqriv	$⊢ U = Unit (S)$

Metamath Proof Explorer

Theorem opprunit

Proof