opprdomn

Description: The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015)

		Ref	Expression
	Hypothesis	opprdomn.1	$⊢ O = {opp}_{r} (R)$
	Assertion	opprdomn	$⊢ R \in Domn \to O \in Domn$

Proof

Step	Hyp	Ref	Expression
1		opprdomn.1	$⊢ O = {opp}_{r} (R)$
2		domnnzr	$⊢ R \in Domn \to R \in NzRing$
3	1	opprnzr	$⊢ R \in NzRing \to O \in NzRing$
4	2 3	syl	$⊢ R \in Domn \to O \in NzRing$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	5 6 7	domneq0	$⊢ (R \in Domn \land y \in {Base}_{R} \land x \in {Base}_{R}) \to (y \cdot_{R} x = 0_{R} \leftrightarrow (y = 0_{R} \lor x = 0_{R}))$
9	8	3com23	$⊢ (R \in Domn \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (y \cdot_{R} x = 0_{R} \leftrightarrow (y = 0_{R} \lor x = 0_{R}))$
10		eqid	$⊢ \cdot_{O} = \cdot_{O}$
11	5 6 1 10	opprmul	$⊢ x \cdot_{O} y = y \cdot_{R} x$
12	11	eqeq1i	$⊢ x \cdot_{O} y = 0_{R} \leftrightarrow y \cdot_{R} x = 0_{R}$
13		orcom	$⊢ (x = 0_{R} \lor y = 0_{R}) \leftrightarrow (y = 0_{R} \lor x = 0_{R})$
14	9 12 13	3bitr4g	$⊢ (R \in Domn \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (x \cdot_{O} y = 0_{R} \leftrightarrow (x = 0_{R} \lor y = 0_{R}))$
15	14	biimpd	$⊢ (R \in Domn \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (x \cdot_{O} y = 0_{R} \to (x = 0_{R} \lor y = 0_{R}))$
16	15	3expb	$⊢ (R \in Domn \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (x \cdot_{O} y = 0_{R} \to (x = 0_{R} \lor y = 0_{R}))$
17	16	ralrimivva	$⊢ R \in Domn \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{O} y = 0_{R} \to (x = 0_{R} \lor y = 0_{R}))$
18	1 5	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
19	1 7	oppr0	$⊢ 0_{R} = 0_{O}$
20	18 10 19	isdomn	$⊢ O \in Domn \leftrightarrow (O \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{O} y = 0_{R} \to (x = 0_{R} \lor y = 0_{R})))$
21	4 17 20	sylanbrc	$⊢ R \in Domn \to O \in Domn$

Metamath Proof Explorer

Theorem opprdomn

Proof