opprdrng

Description: The opposite of a division ring is also a division ring. (Contributed by NM, 18-Oct-2014)

		Ref	Expression
	Hypothesis	opprdrng.1	$⊢ O = {opp}_{r} (R)$
	Assertion	opprdrng	$⊢ R \in DivRing \leftrightarrow O \in DivRing$

Step	Hyp	Ref	Expression
1		opprdrng.1	$⊢ O = {opp}_{r} (R)$
2	1	opprringb	$⊢ R \in Ring \leftrightarrow O \in Ring$
3	2	anbi1i	$⊢ (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\}) \leftrightarrow (O \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ Unit (R) = Unit (R)$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	4 5 6	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
8	1 4	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
9	5 1	opprunit	$⊢ Unit (R) = Unit (O)$
10	1 6	oppr0	$⊢ 0_{R} = 0_{O}$
11	8 9 10	isdrng	$⊢ O \in DivRing \leftrightarrow (O \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
12	3 7 11	3bitr4i	$⊢ R \in DivRing \leftrightarrow O \in DivRing$

Metamath Proof Explorer